consider A1 being set such that
for x, y being Variable holds
( [(x '=' y),F₁(x,y)] in A1 & [(x 'in' y),F₂(x,y)] in A1 ) and
A3: [F₆(),F₇()] in A1 and
A4: for H being ZF-formula
for a being set st [H,a] in A1 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 A1 ) ) & ( H is conjunctive implies ex b, c being set st
( a = F₄(b,c) & [(the_left_argument_of H),b] in A1 & [(the_right_argument_of H),c] in A1 ) ) & ( H is universal implies ex b being set st
( a = F₅((bound_in H),b) & [(the_scope_of H),b] in A1 ) ) ) by A1;
consider A2 being set such that
for x, y being Variable holds
( [(x '=' y),F₁(x,y)] in A2 & [(x 'in' y),F₂(x,y)] in A2 ) and
A5: [F₆(),F₈()] in A2 and
A6: for H being ZF-formula
for a being set st [H,a] in A2 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 A2 ) ) & ( H is conjunctive implies ex b, c being set st
( a = F₄(b,c) & [(the_left_argument_of H),b] in A2 & [(the_right_argument_of H),c] in A2 ) ) & ( H is universal implies ex b being set st
( a = F₅((bound_in H),b) & [(the_scope_of H),b] in A2 ) ) ) by A2;
defpred S₁[ ZF-formula] means for a, b being set st [$1,a] in A1 & [$1,b] in A2 holds
a = b;
A7: for H being ZF-formula st H is atomic holds
S₁[H]

proof

let H be ZF-formula; :: thesis: ( H is atomic implies S₁[H] )
assume A8: ( H is being_equality or H is being_membership ) ; :: according to ZF_LANG:def 15 :: thesis: S₁[H]
let a, b be set ; :: thesis: ( [H,a] in A1 & [H,b] in A2 implies a = b )
assume A9: ( [H,a] in A1 & [H,b] in A2 ) ; :: thesis: a = b

A10: now

assume H is being_equality ; :: thesis: a = b
then ( a = F₁((Var1 H),(Var2 H)) & b = F₁((Var1 H),(Var2 H)) ) by A4, A6, A9;
hence a = b ; :: thesis: verum

end;

now

assume H is being_membership ; :: thesis: a = b
then ( a = F₂((Var1 H),(Var2 H)) & b = F₂((Var1 H),(Var2 H)) ) by A4, A6, A9;
hence a = b ; :: thesis: verum

end;

hence a = b by A8, A10; :: thesis: verum

end;

A11: for H being ZF-formula st H is negative & S₁[ the_argument_of H] holds
S₁[H]

proof

let H be ZF-formula; :: thesis: ( H is negative & S₁[ the_argument_of H] implies S₁[H] )
assume that
A12: H is negative and
A13: for a, b being set st [(the_argument_of H),a] in A1 & [(the_argument_of H),b] in A2 holds
a = b ; :: thesis: S₁[H]
let a, b be set ; :: thesis: ( [H,a] in A1 & [H,b] in A2 implies a = b )
assume A14: ( [H,a] in A1 & [H,b] in A2 ) ; :: thesis: a = b
then A15: ex a1 being set st
( a = F₃(a1) & [(the_argument_of H),a1] in A1 ) by A4, A12;
ex b1 being set st
( b = F₃(b1) & [(the_argument_of H),b1] in A2 ) by A6, A12, A14;
hence a = b by A13, A15; :: thesis: verum

end;

A16: for H being ZF-formula st H is conjunctive & S₁[ the_left_argument_of H] & S₁[ the_right_argument_of H] holds
S₁[H]

proof

let H be ZF-formula; :: thesis: ( H is conjunctive & S₁[ the_left_argument_of H] & S₁[ the_right_argument_of H] implies S₁[H] )
assume that
A17: H is conjunctive and
A18: for a, b being set st [(the_left_argument_of H),a] in A1 & [(the_left_argument_of H),b] in A2 holds
a = b and
A19: for a, b being set st [(the_right_argument_of H),a] in A1 & [(the_right_argument_of H),b] in A2 holds
a = b ; :: thesis: S₁[H]
let a, b be set ; :: thesis: ( [H,a] in A1 & [H,b] in A2 implies a = b )
assume A20: ( [H,a] in A1 & [H,b] in A2 ) ; :: thesis: a = b
then consider a1, a2 being set such that
A21: ( a = F₄(a1,a2) & [(the_left_argument_of H),a1] in A1 & [(the_right_argument_of H),a2] in A1 ) by A4, A17;
consider b1, b2 being set such that
A22: ( b = F₄(b1,b2) & [(the_left_argument_of H),b1] in A2 & [(the_right_argument_of H),b2] in A2 ) by A6, A17, A20;
( a1 = b1 & a2 = b2 ) by A18, A19, A21, A22;
hence a = b by A21, A22; :: thesis: verum

end;

A23: for H being ZF-formula st H is universal & S₁[ the_scope_of H] holds
S₁[H]

proof

let H be ZF-formula; :: thesis: ( H is universal & S₁[ the_scope_of H] implies S₁[H] )
assume that
A24: H is universal and
A25: for a, b being set st [(the_scope_of H),a] in A1 & [(the_scope_of H),b] in A2 holds
a = b ; :: thesis: S₁[H]
let a, b be set ; :: thesis: ( [H,a] in A1 & [H,b] in A2 implies a = b )
assume A26: ( [H,a] in A1 & [H,b] in A2 ) ; :: thesis: a = b
then A27: ex a1 being set st
( a = F₅((bound_in H),a1) & [(the_scope_of H),a1] in A1 ) by A4, A24;
ex b1 being set st
( b = F₅((bound_in H),b1) & [(the_scope_of H),b1] in A2 ) by A6, A24, A26;
hence a = b by A25, A27; :: thesis: verum

end;

for H being ZF-formula holds S₁[H] from ZF_LANG:sch 1(A7, A11, A16, A23);
hence F₇() = F₈() by A3, A5; :: thesis: verum