let M be non empty set ; :: thesis: for H being ZF-formula
for v being Function of VAR ,M st not x. 0 in Free H holds
( M,v |= All (x. 3),(Ex (x. 0 ),(All (x. 4),(H <=> ((x. 4) '=' (x. 0 ))))) iff for m1 being Element of M ex m2 being Element of M st
for m3 being Element of M holds
( M,(v / (x. 3),m1) / (x. 4),m3 |= H iff m3 = m2 ) )
let H be ZF-formula; :: thesis: for v being Function of VAR ,M st not x. 0 in Free H holds
( M,v |= All (x. 3),(Ex (x. 0 ),(All (x. 4),(H <=> ((x. 4) '=' (x. 0 ))))) iff for m1 being Element of M ex m2 being Element of M st
for m3 being Element of M holds
( M,(v / (x. 3),m1) / (x. 4),m3 |= H iff m3 = m2 ) )
let v be Function of VAR ,M; :: thesis: ( not x. 0 in Free H implies ( M,v |= All (x. 3),(Ex (x. 0 ),(All (x. 4),(H <=> ((x. 4) '=' (x. 0 ))))) iff for m1 being Element of M ex m2 being Element of M st
for m3 being Element of M holds
( M,(v / (x. 3),m1) / (x. 4),m3 |= H iff m3 = m2 ) ) )
assume A1: not x. 0 in Free H ; :: thesis: ( M,v |= All (x. 3),(Ex (x. 0 ),(All (x. 4),(H <=> ((x. 4) '=' (x. 0 ))))) iff for m1 being Element of M ex m2 being Element of M st
for m3 being Element of M holds
( M,(v / (x. 3),m1) / (x. 4),m3 |= H iff m3 = m2 ) )
thus ( M,v |= All (x. 3),(Ex (x. 0 ),(All (x. 4),(H <=> ((x. 4) '=' (x. 0 ))))) implies for m1 being Element of M ex m2 being Element of M st
for m3 being Element of M holds
( M,(v / (x. 3),m1) / (x. 4),m3 |= H iff m3 = m2 ) ) :: thesis: ( ( for m1 being Element of M ex m2 being Element of M st
for m3 being Element of M holds
( M,(v / (x. 3),m1) / (x. 4),m3 |= H iff m3 = m2 ) ) implies M,v |= All (x. 3),(Ex (x. 0 ),(All (x. 4),(H <=> ((x. 4) '=' (x. 0 ))))) )

proof

assume A2: M,v |= All (x. 3),(Ex (x. 0 ),(All (x. 4),(H <=> ((x. 4) '=' (x. 0 ))))) ; :: thesis: for m1 being Element of M ex m2 being Element of M st
for m3 being Element of M holds
( M,(v / (x. 3),m1) / (x. 4),m3 |= H iff m3 = m2 )
let m1 be Element of M; :: thesis: ex m2 being Element of M st
for m3 being Element of M holds
( M,(v / (x. 3),m1) / (x. 4),m3 |= H iff m3 = m2 )
M,v / (x. 3),m1 |= Ex (x. 0 ),(All (x. 4),(H <=> ((x. 4) '=' (x. 0 )))) by A2, ZF_LANG1:80;
then consider m2 being Element of M such that
A3: M,(v / (x. 3),m1) / (x. 0 ),m2 |= All (x. 4),(H <=> ((x. 4) '=' (x. 0 ))) by ZF_LANG1:82;
take m2 ; :: thesis: for m3 being Element of M holds
( M,(v / (x. 3),m1) / (x. 4),m3 |= H iff m3 = m2 )
let m3 be Element of M; :: thesis: ( M,(v / (x. 3),m1) / (x. 4),m3 |= H iff m3 = m2 )
thus ( M,(v / (x. 3),m1) / (x. 4),m3 |= H implies m3 = m2 ) :: thesis: ( m3 = m2 implies M,(v / (x. 3),m1) / (x. 4),m3 |= H )

proof

assume M,(v / (x. 3),m1) / (x. 4),m3 |= H ; :: thesis: m3 = m2
then M,((v / (x. 3),m1) / (x. 4),m3) / (x. 0 ),m2 |= H by A1, Th10;
then A4: M,((v / (x. 3),m1) / (x. 0 ),m2) / (x. 4),m3 |= H by FUNCT_7:35, ZF_LANG1:86;
M,((v / (x. 3),m1) / (x. 0 ),m2) / (x. 4),m3 |= H <=> ((x. 4) '=' (x. 0 )) by A3, ZF_LANG1:80;
then A5: M,((v / (x. 3),m1) / (x. 0 ),m2) / (x. 4),m3 |= (x. 4) '=' (x. 0 ) by A4, ZF_MODEL:19;
A6: m2 = ((v / (x. 3),m1) / (x. 0 ),m2) . (x. 0 ) by FUNCT_7:130;
A7: (((v / (x. 3),m1) / (x. 0 ),m2) / (x. 4),m3) . (x. 0 ) = ((v / (x. 3),m1) / (x. 0 ),m2) . (x. 0 ) by FUNCT_7:34, ZF_LANG1:86;
(((v / (x. 3),m1) / (x. 0 ),m2) / (x. 4),m3) . (x. 4) = m3 by FUNCT_7:130;
hence m3 = m2 by A6, A7, A5, ZF_MODEL:12; :: thesis: verum

end;

assume m3 = m2 ; :: thesis: M,(v / (x. 3),m1) / (x. 4),m3 |= H
then A8: M,((v / (x. 3),m1) / (x. 0 ),m3) / (x. 4),m3 |= H <=> ((x. 4) '=' (x. 0 )) by A3, ZF_LANG1:80;
A9: (((v / (x. 3),m1) / (x. 0 ),m3) / (x. 4),m3) . (x. 0 ) = ((v / (x. 3),m1) / (x. 0 ),m3) . (x. 0 ) by FUNCT_7:34, ZF_LANG1:86;
A10: ((v / (x. 3),m1) / (x. 0 ),m3) . (x. 0 ) = m3 by FUNCT_7:130;
(((v / (x. 3),m1) / (x. 0 ),m3) / (x. 4),m3) . (x. 4) = m3 by FUNCT_7:130;
then M,((v / (x. 3),m1) / (x. 0 ),m3) / (x. 4),m3 |= (x. 4) '=' (x. 0 ) by A9, A10, ZF_MODEL:12;
then M,((v / (x. 3),m1) / (x. 0 ),m3) / (x. 4),m3 |= H by A8, ZF_MODEL:19;
then M,((v / (x. 3),m1) / (x. 4),m3) / (x. 0 ),m3 |= H by FUNCT_7:35, ZF_LANG1:86;
hence M,(v / (x. 3),m1) / (x. 4),m3 |= H by A1, Th10; :: thesis: verum

end;

assume A11: for m1 being Element of M ex m2 being Element of M st
for m3 being Element of M holds
( M,(v / (x. 3),m1) / (x. 4),m3 |= H iff m3 = m2 ) ; :: thesis: M,v |= All (x. 3),(Ex (x. 0 ),(All (x. 4),(H <=> ((x. 4) '=' (x. 0 )))))

now

let m1 be Element of M; :: thesis: M,v / (x. 3),m1 |= Ex (x. 0 ),(All (x. 4),(H <=> ((x. 4) '=' (x. 0 ))))
consider m2 being Element of M such that
A12: for m3 being Element of M holds
( M,(v / (x. 3),m1) / (x. 4),m3 |= H iff m3 = m2 ) by A11;

now

let m3 be Element of M; :: thesis: M,((v / (x. 3),m1) / (x. 0 ),m2) / (x. 4),m3 |= H <=> ((x. 4) '=' (x. 0 ))
A13: (((v / (x. 3),m1) / (x. 0 ),m2) / (x. 4),m3) . (x. 0 ) = ((v / (x. 3),m1) / (x. 0 ),m2) . (x. 0 ) by FUNCT_7:34, ZF_LANG1:86;
A14: ((v / (x. 3),m1) / (x. 0 ),m2) . (x. 0 ) = m2 by FUNCT_7:130;
A15: (((v / (x. 3),m1) / (x. 0 ),m2) / (x. 4),m3) . (x. 4) = m3 by FUNCT_7:130;

A16: now

assume M,((v / (x. 3),m1) / (x. 0 ),m2) / (x. 4),m3 |= (x. 4) '=' (x. 0 ) ; :: thesis: M,((v / (x. 3),m1) / (x. 0 ),m2) / (x. 4),m3 |= H
then m3 = m2 by A15, A13, A14, ZF_MODEL:12;
then M,(v / (x. 3),m1) / (x. 4),m3 |= H by A12;
then M,((v / (x. 3),m1) / (x. 4),m3) / (x. 0 ),m2 |= H by A1, Th10;
hence M,((v / (x. 3),m1) / (x. 0 ),m2) / (x. 4),m3 |= H by FUNCT_7:35, ZF_LANG1:86; :: thesis: verum

end;

now

assume M,((v / (x. 3),m1) / (x. 0 ),m2) / (x. 4),m3 |= H ; :: thesis: M,((v / (x. 3),m1) / (x. 0 ),m2) / (x. 4),m3 |= (x. 4) '=' (x. 0 )
then M,((v / (x. 3),m1) / (x. 4),m3) / (x. 0 ),m2 |= H by FUNCT_7:35, ZF_LANG1:86;
then M,(v / (x. 3),m1) / (x. 4),m3 |= H by A1, Th10;
then m3 = m2 by A12;
hence M,((v / (x. 3),m1) / (x. 0 ),m2) / (x. 4),m3 |= (x. 4) '=' (x. 0 ) by A15, A13, A14, ZF_MODEL:12; :: thesis: verum

end;

hence M,((v / (x. 3),m1) / (x. 0 ),m2) / (x. 4),m3 |= H <=> ((x. 4) '=' (x. 0 )) by A16, ZF_MODEL:19; :: thesis: verum

end;

then M,(v / (x. 3),m1) / (x. 0 ),m2 |= All (x. 4),(H <=> ((x. 4) '=' (x. 0 ))) by ZF_LANG1:80;
hence M,v / (x. 3),m1 |= Ex (x. 0 ),(All (x. 4),(H <=> ((x. 4) '=' (x. 0 )))) by ZF_LANG1:82; :: thesis: verum

end;

hence M,v |= All (x. 3),(Ex (x. 0 ),(All (x. 4),(H <=> ((x. 4) '=' (x. 0 ))))) by ZF_LANG1:80; :: thesis: verum