scheme :: ZF_MODEL:sch 3
ZFschresult{ F₁( Variable, Variable) -> set , F₂( Variable, Variable) -> set , F₃( set ) -> set , F₄( set , set ) -> set , F₅( Variable, set ) -> set , F₆() -> ZF-formula, F₇( ZF-formula) -> set } :

( ( F₆() is being_equality implies F₇(F₆()) = F₁((Var1 F₆()),(Var2 F₆())) ) & ( F₆() is being_membership implies F₇(F₆()) = F₂((Var1 F₆()),(Var2 F₆())) ) & ( F₆() is negative implies F₇(F₆()) = F₃(F₇((the_argument_of F₆()))) ) & ( F₆() is conjunctive implies for a, b being set st a = F₇((the_left_argument_of F₆())) & b = F₇((the_right_argument_of F₆())) holds
F₇(F₆()) = F₄(a,b) ) & ( F₆() is universal implies F₇(F₆()) = F₅((bound_in F₆()),F₇((the_scope_of F₆()))) ) )

provided

A1: for H9 being ZF-formula
for a being set holds
( a = F₇(H9) iff ex A being set st
( ( for x, y being Variable holds
( [(x '=' y),F₁(x,y)] in A & [(x 'in' y),F₂(x,y)] in A ) ) & [H9,a] in A & ( for H being ZF-formula
for a being set st [H,a] in A holds
( ( H is being_equality implies a = F₁((Var1 H),(Var2 H)) ) & ( H is being_membership implies a = F₂((Var1 H),(Var2 H)) ) & ( H is negative implies ex b being set st
( a = F₃(b) & [(the_argument_of H),b] in A ) ) & ( H is conjunctive implies ex b, c being set st
( a = F₄(b,c) & [(the_left_argument_of H),b] in A & [(the_right_argument_of H),c] in A ) ) & ( H is universal implies ex b being set st
( a = F₅((bound_in H),b) & [(the_scope_of H),b] in A ) ) ) ) ) )