:: deftheorem Def1 defines Free ZF_MODEL:def 1 :
for H being ZF-formula
for b₂ being set holds
( b₂ = Free H iff ex A being set st
( ( for x, y being Variable holds
( [(x '=' y),{x,y}] in A & [(x 'in' y),{x,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 = {(Var1 H9),(Var2 H9)} ) & ( H9 is being_membership implies a = {(Var1 H9),(Var2 H9)} ) & ( H9 is negative implies ex b being set st
( a = b & [(the_argument_of H9),b] in A ) ) & ( H9 is conjunctive implies ex b, c being set st
( a = union {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 = b \ {(bound_in H9)} & [(the_scope_of H9),b] in A ) ) ) ) ) );