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:23;
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)

A5: 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))
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: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

consider g being 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 = g +* (x. 0 ),X;
A9: (g +* (x. 0 ),X) . (x. 0 ) = X by FUNCT_7:130;
A10: ( x. 0 = 5 + 0 & x. 1 = 5 + 1 ) by ZF_LANG:def 2;
set f = (g +* (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 <> ((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 A13: ( 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, 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:34, FUNCT_7:130; :: thesis: verum

end;

( ((g +* (x. 0 ),X) +* (x. 1),Y) . (x. 1) = Y & ((g +* (x. 0 ),X) +* (x. 1),Y) . (x. 0 ) = (g +* (x. 0 ),X) . (x. 0 ) ) by A10, FUNCT_7:34, FUNCT_7:130;
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