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 )
A1: 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:23;
assume 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
then 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:25, ZF_MODEL:def 6;
then A2: E |= (All (x. 2),(((x. 2) 'in' (x. 0 )) <=> ((x. 2) 'in' (x. 1)))) => ((x. 0 ) '=' (x. 1)) by ZF_MODEL:25;
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)
E,f |= (All (x. 2),(((x. 2) 'in' (x. 0 )) <=> ((x. 2) 'in' (x. 1)))) => ((x. 0 ) '=' (x. 1)) by A2, ZF_MODEL:def 5;
then A5: ( 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;

now

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))
( ( g . (x. 2) in g . (x. 0 ) implies E,g |= (x. 2) 'in' (x. 0 ) ) & ( E,g |= (x. 2) 'in' (x. 0 ) implies g . (x. 2) in g . (x. 0 ) ) & ( g . (x. 2) in g . (x. 1) implies E,g |= (x. 2) 'in' (x. 1) ) & ( E,g |= (x. 2) 'in' (x. 1) implies g . (x. 2) in g . (x. 1) ) & not ( ( E,g |= (x. 2) 'in' (x. 0 ) implies E,g |= (x. 2) 'in' (x. 1) ) & ( E,g |= (x. 2) 'in' (x. 1) implies E,g |= (x. 2) 'in' (x. 0 ) ) & not E,g |= ((x. 2) 'in' (x. 0 )) <=> ((x. 2) 'in' (x. 1)) ) & ( E,g |= ((x. 2) 'in' (x. 0 )) <=> ((x. 2) 'in' (x. 1)) implies ( E,g |= (x. 2) 'in' (x. 0 ) iff E,g |= (x. 2) 'in' (x. 1) ) ) ) by ZF_MODEL:13, ZF_MODEL:19;
hence E,g |= ((x. 2) 'in' (x. 0 )) <=> ((x. 2) 'in' (x. 1)) by A4, A6; :: thesis: verum

end;

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

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 A7: for Z being Element of E holds
( Z in X iff Z in Y ) ; :: thesis: X = Y
consider g being Function of VAR ,E;
set g0 = g +* (x. 0 ),X;
A8: (g +* (x. 0 ),X) . (x. 0 ) = X by FUNCT_7:130;
set f = (g +* (x. 0 ),X) +* (x. 1),Y;
A9: ((g +* (x. 0 ),X) +* (x. 1),Y) . (x. 1) = Y by FUNCT_7:130;
A10: ( x. 0 = 5 + 0 & x. 1 = 5 + 1 & x. 2 = 5 + 2 ) by ZF_LANG:def 2;
then A11: ( x. 0 <> x. 2 & x. 1 <> x. 2 & ((g +* (x. 0 ),X) +* (x. 1),Y) . (x. 0 ) = (g +* (x. 0 ),X) . (x. 0 ) ) by FUNCT_7:34;
for h being Function of VAR ,E st ( for x being Variable st h . x <> ((g +* (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 <> ((g +* (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 <> ((g +* (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 A12: ( h . (x. 0 ) = ((g +* (x. 0 ),X) +* (x. 1),Y) . (x. 0 ) & h . (x. 1) = ((g +* (x. 0 ),X) +* (x. 1),Y) . (x. 1) ) by A10;
( h . (x. 2) in X iff h . (x. 2) in Y ) by A7;
hence ( h . (x. 2) in h . (x. 0 ) iff h . (x. 2) in h . (x. 1) ) by A8, FUNCT_7:130, A12, FUNCT_7:34; :: thesis: verum

end;

hence X = Y by A3, A8, A9, A11; :: 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