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 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
A8: H is universal and
A9: 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 ( [H,a] in A1 & [H,b] in A2 ) ; :: thesis: a = b
then ( ex a1 being set st
( a = F₅((bound_in H),a1) & [(the_scope_of H),a1] in A1 ) & ex b1 being set st
( b = F₅((bound_in H),b1) & [(the_scope_of H),b1] in A2 ) ) by A4, A6, A8;
hence a = b by A9; :: thesis: verum

end;

A10: 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 A11: ( 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 that
A12: [H,a] in A1 and
A13: [H,b] in A2 ; :: thesis: a = b

A14: now :: thesis: ( H is being_membership implies a = b )

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

end;

now :: thesis: ( H is being_equality implies a = b )

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

end;

hence a = b by A11, A14; :: thesis: verum

end;

A17: 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
A18: H is conjunctive and
A19: 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
A20: 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 that
A21: [H,a] in A1 and
A22: [H,b] in A2 ; :: thesis: a = b
consider a1, a2 being set such that
A23: a = F₄(a1,a2) and
A24: [(the_left_argument_of H),a1] in A1 and
A25: [(the_right_argument_of H),a2] in A1 by A4, A18, A21;
consider b1, b2 being set such that
A26: b = F₄(b1,b2) and
A27: [(the_left_argument_of H),b1] in A2 and
A28: [(the_right_argument_of H),b2] in A2 by A6, A18, A22;
a1 = b1 by A19, A24, A27;
hence a = b by A20, A23, A25, A26, A28; :: thesis: verum

end;

A29: 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
A30: H is negative and
A31: 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 ( [H,a] in A1 & [H,b] in A2 ) ; :: thesis: a = b
then ( ex a1 being set st
( a = F₃(a1) & [(the_argument_of H),a1] in A1 ) & ex b1 being set st
( b = F₃(b1) & [(the_argument_of H),b1] in A2 ) ) by A4, A6, A30;
hence a = b by A31; :: thesis: verum

end;

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