:: deftheorem Def3 defines St ZF_MODEL:def 3 :
for H being ZF-formula
for E being non empty set
for b₃ being set holds
( b₃ = St (H,E) iff ex A being set st
( ( for x, y being Variable holds
( [(x '=' y), { v1 where v1 is Element of VAL E : for f being Function of VAR,E st f = v1 holds
f . x = f . y } ] in A & [(x 'in' y), { v2 where v2 is Element of VAL E : for f being Function of VAR,E st f = v2 holds
f . x in f . y } ] in A ) ) & [H,b₃] in A & ( for H9 being ZF-formula
for a being set st [H9,a] in A holds
( ( H9 is being_equality implies a = { v3 where v3 is Element of VAL E : for f being Function of VAR,E st f = v3 holds
f . (Var1 H9) = f . (Var2 H9) } ) & ( H9 is being_membership implies a = { v4 where v4 is Element of VAL E : for f being Function of VAR,E st f = v4 holds
f . (Var1 H9) in f . (Var2 H9) } ) & ( H9 is negative implies ex b being set st
( a = (VAL E) \ b & [(the_argument_of H9),b] in A ) ) & ( H9 is conjunctive implies ex b, c being set st
( a = b /\ c & [(the_left_argument_of H9),b] in A & [(the_right_argument_of H9),c] in A ) ) & ( H9 is universal implies ex b being set st
( a = { v5 where v5 is Element of VAL E : for X being set
for f being Function of VAR,E st X = b & f = v5 holds
( f in X & ( for g being Function of VAR,E st ( for y being Variable st g . y <> f . y holds
bound_in H9 = y ) holds
g in X ) ) } & [(the_scope_of H9),b] in A ) ) ) ) ) );