consider A1 being set such that
for x, y being Variable holds
( [(x '=' y),F1(x,y)] in A1 & [(x 'in' y),F2(x,y)] in A1 ) and
A3: [F6(),F7()] 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 = F1((Var1 H),(Var2 H)) ) & ( H is being_membership implies a = F2((Var1 H),(Var2 H)) ) & ( H is negative implies ex b being set st
( a = F3(b) & [(the_argument_of H),b] in A1 ) ) & ( H is conjunctive implies ex b, c being set st
( a = F4(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 = F5((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),F1(x,y)] in A2 & [(x 'in' y),F2(x,y)] in A2 ) and
A5: [F6(),F8()] 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 = F1((Var1 H),(Var2 H)) ) & ( H is being_membership implies a = F2((Var1 H),(Var2 H)) ) & ( H is negative implies ex b being set st
( a = F3(b) & [(the_argument_of H),b] in A2 ) ) & ( H is conjunctive implies ex b, c being set st
( a = F4(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 = F5((bound_in H),b) & [(the_scope_of H),b] in A2 ) ) ) by A2;
defpred S1[ 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 & S1[ the_scope_of H] holds
S1[H]
proof
let H be ZF-formula; :: thesis: ( H is universal & S1[ the_scope_of H] implies S1[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: S1[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 = F5((bound_in H),a1) & [(the_scope_of H),a1] in A1 ) & ex b1 being set st
( b = F5((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
S1[H]
proof
let H be ZF-formula; :: thesis: ( H is atomic implies S1[H] )
assume A11: ( H is being_equality or H is being_membership ) ; :: according to ZF_LANG:def 15 :: thesis: S1[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 = F2((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 = F1((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 & S1[ the_left_argument_of H] & S1[ the_right_argument_of H] holds
S1[H]
proof
let H be ZF-formula; :: thesis: ( H is conjunctive & S1[ the_left_argument_of H] & S1[ the_right_argument_of H] implies S1[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: S1[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 = F4(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 = F4(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 & S1[ the_argument_of H] holds
S1[H]
proof
let H be ZF-formula; :: thesis: ( H is negative & S1[ the_argument_of H] implies S1[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: S1[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 = F3(a1) & [(the_argument_of H),a1] in A1 ) & ex b1 being set st
( b = F3(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 S1[H] from ZF_LANG:sch 1(A10, A29, A17, A7);
 hence F7() = F8() by A3, A5; :: thesis: verum