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

ex a, 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 ) ) & [F₆(),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 ) ) ) ) )