let E be non empty set ; :: thesis: ( E |= the_axiom_of_extensionality implies for u, v being Element of E st ( for w being Element of E holds
( w in u iff w in v ) ) holds
u = v )
assume A1: E |= the_axiom_of_extensionality ; :: thesis: for u, v being Element of E st ( for w being Element of E holds
( w in u iff w in v ) ) holds
u = v
All ((x. 0),(All ((x. 1),((All ((x. 2),(((x. 2) 'in' (x. 0)) <=> ((x. 2) 'in' (x. 1))))) => ((x. 0) '=' (x. 1)))))) = All ((x. 0),(x. 1),((All ((x. 2),(((x. 2) 'in' (x. 0)) <=> ((x. 2) 'in' (x. 1))))) => ((x. 0) '=' (x. 1)))) by ZF_LANG:7;
then A2: E |= All ((x. 1),((All ((x. 2),(((x. 2) 'in' (x. 0)) <=> ((x. 2) 'in' (x. 1))))) => ((x. 0) '=' (x. 1)))) by A1, ZF_MODEL:23, ZF_MODEL:def 6;
A3: for f being Function of VAR,E st ( for g being Function of VAR,E st ( for x being Variable st g . x <> f . x holds
x. 2 = x ) holds
( g . (x. 2) in g . (x. 0) iff g . (x. 2) in g . (x. 1) ) ) holds
f . (x. 0) = f . (x. 1)

proof

let f be Function of VAR,E; :: thesis: ( ( for g being Function of VAR,E st ( for x being Variable st g . x <> f . x holds
x. 2 = x ) holds
( g . (x. 2) in g . (x. 0) iff g . (x. 2) in g . (x. 1) ) ) implies f . (x. 0) = f . (x. 1) )
assume A4: for g being Function of VAR,E st ( for x being Variable st g . x <> f . x holds
x. 2 = x ) holds
( g . (x. 2) in g . (x. 0) iff g . (x. 2) in g . (x. 1) ) ; :: thesis: f . (x. 0) = f . (x. 1)

A5: now :: thesis: for g being Function of VAR,E st ( for x being Variable st g . x <> f . x holds
x. 2 = x ) holds
E,g |= ((x. 2) 'in' (x. 0)) <=> ((x. 2) 'in' (x. 1))

let g be Function of VAR,E; :: thesis: ( ( for x being Variable st g . x <> f . x holds
x. 2 = x ) implies E,g |= ((x. 2) 'in' (x. 0)) <=> ((x. 2) 'in' (x. 1)) )
assume A6: for x being Variable st g . x <> f . x holds
x. 2 = x ; :: thesis: E,g |= ((x. 2) 'in' (x. 0)) <=> ((x. 2) 'in' (x. 1))
A7: ( g . (x. 2) in g . (x. 1) iff E,g |= (x. 2) 'in' (x. 1) ) by ZF_MODEL:13;
( g . (x. 2) in g . (x. 0) iff E,g |= (x. 2) 'in' (x. 0) ) by ZF_MODEL:13;
hence E,g |= ((x. 2) 'in' (x. 0)) <=> ((x. 2) 'in' (x. 1)) by A4, A6, A7, ZF_MODEL:19; :: thesis: verum

end;

E,f |= (All ((x. 2),(((x. 2) 'in' (x. 0)) <=> ((x. 2) 'in' (x. 1))))) => ((x. 0) '=' (x. 1)) by A2, ZF_MODEL:23, ZF_MODEL:def 5;
then ( E,f |= All ((x. 2),(((x. 2) 'in' (x. 0)) <=> ((x. 2) 'in' (x. 1)))) implies E,f |= (x. 0) '=' (x. 1) ) by ZF_MODEL:18;
hence f . (x. 0) = f . (x. 1) by A5, ZF_MODEL:12, ZF_MODEL:16; :: thesis: verum

end;

for X, Y being Element of E st ( for Z being Element of E holds
( Z in X iff Z in Y ) ) holds
X = Y

proof

set g = the Function of VAR,E;
let X, Y be Element of E; :: thesis: ( ( for Z being Element of E holds
( Z in X iff Z in Y ) ) implies X = Y )
assume A8: for Z being Element of E holds
( Z in X iff Z in Y ) ; :: thesis: X = Y
set g0 = the Function of VAR,E +* ((x. 0),X);
A9: ( the Function of VAR,E +* ((x. 0),X)) . (x. 0) = X by FUNCT_7:128;
A10: ( x. 0 = 5 + 0 & x. 1 = 5 + 1 ) by ZF_LANG:def 2;
set f = ( the Function of VAR,E +* ((x. 0),X)) +* ((x. 1),Y);
A11: x. 2 = 5 + 2 by ZF_LANG:def 2;
A12: for h being Function of VAR,E st ( for x being Variable st h . x <> (( the Function of VAR,E +* ((x. 0),X)) +* ((x. 1),Y)) . x holds
x. 2 = x ) holds
( h . (x. 2) in h . (x. 0) iff h . (x. 2) in h . (x. 1) )

proof

let h be Function of VAR,E; :: thesis: ( ( for x being Variable st h . x <> (( the Function of VAR,E +* ((x. 0),X)) +* ((x. 1),Y)) . x holds
x. 2 = x ) implies ( h . (x. 2) in h . (x. 0) iff h . (x. 2) in h . (x. 1) ) )
assume for x being Variable st h . x <> (( the Function of VAR,E +* ((x. 0),X)) +* ((x. 1),Y)) . x holds
x. 2 = x ; :: thesis: ( h . (x. 2) in h . (x. 0) iff h . (x. 2) in h . (x. 1) )
then A13: ( h . (x. 0) = (( the Function of VAR,E +* ((x. 0),X)) +* ((x. 1),Y)) . (x. 0) & h . (x. 1) = (( the Function of VAR,E +* ((x. 0),X)) +* ((x. 1),Y)) . (x. 1) ) by A10, A11;
( h . (x. 2) in X iff h . (x. 2) in Y ) by A8;
hence ( h . (x. 2) in h . (x. 0) iff h . (x. 2) in h . (x. 1) ) by A9, A13, FUNCT_7:32, FUNCT_7:128; :: thesis: verum

end;

( (( the Function of VAR,E +* ((x. 0),X)) +* ((x. 1),Y)) . (x. 1) = Y & (( the Function of VAR,E +* ((x. 0),X)) +* ((x. 1),Y)) . (x. 0) = ( the Function of VAR,E +* ((x. 0),X)) . (x. 0) ) by A10, FUNCT_7:32, FUNCT_7:128;
hence X = Y by A3, A9, A12; :: thesis: verum

end;

hence for u, v being Element of E st ( for w being Element of E holds
( w in u iff w in v ) ) holds
u = v ; :: thesis: verum