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 ( M,((v / (x. 3),m1) / (x. 0 ),m2) / (x. 4),m3 |= H <=> ((x. 4) '=' (x. 0 )) & M,((v / (x. 3),m1) / (x. 0 ),m2) / (x. 4),m3 |= H ) by A3, Lm1, FUNCT_7:35, ZF_LANG1:80;
then ( (((v / (x. 3),m1) / (x. 0 ),m2) / (x. 4),m3) . (x. 4) = m3 & m2 = ((v / (x. 3),m1) / (x. 0 ),m2) . (x. 0 ) & (((v / (x. 3),m1) / (x. 0 ),m2) / (x. 4),m3) . (x. 0 ) = ((v / (x. 3),m1) / (x. 0 ),m2) . (x. 0 ) & M,((v / (x. 3),m1) / (x. 0 ),m2) / (x. 4),m3 |= (x. 4) '=' (x. 0 ) ) by Lm1, FUNCT_7:34, FUNCT_7:130, ZF_MODEL:19;
hence m3 = m2 by ZF_MODEL:12; :: thesis: verum

end;

( (((v / (x. 3),m1) / (x. 0 ),m3) / (x. 4),m3) . (x. 4) = m3 & (((v / (x. 3),m1) / (x. 0 ),m3) / (x. 4),m3) . (x. 0 ) = ((v / (x. 3),m1) / (x. 0 ),m3) . (x. 0 ) & ((v / (x. 3),m1) / (x. 0 ),m3) . (x. 0 ) = m3 ) by Lm1, FUNCT_7:34, FUNCT_7:130;
then A4: M,((v / (x. 3),m1) / (x. 0 ),m3) / (x. 4),m3 |= (x. 4) '=' (x. 0 ) by ZF_MODEL:12;
assume m3 = m2 ; :: thesis: M,(v / (x. 3),m1) / (x. 4),m3 |= H
then M,((v / (x. 3),m1) / (x. 0 ),m3) / (x. 4),m3 |= H <=> ((x. 4) '=' (x. 0 )) by A3, ZF_LANG1:80;
then M,((v / (x. 3),m1) / (x. 0 ),m3) / (x. 4),m3 |= H by A4, 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 A5: 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
A6: for m3 being Element of M holds
( M,(v / (x. 3),m1) / (x. 4),m3 |= H iff m3 = m2 ) by A5;

now

let m3 be Element of M; :: thesis: M,((v / (x. 3),m1) / (x. 0 ),m2) / (x. 4),m3 |= H <=> ((x. 4) '=' (x. 0 ))
A7: ( (((v / (x. 3),m1) / (x. 0 ),m2) / (x. 4),m3) . (x. 4) = m3 & (((v / (x. 3),m1) / (x. 0 ),m2) / (x. 4),m3) . (x. 0 ) = ((v / (x. 3),m1) / (x. 0 ),m2) . (x. 0 ) & ((v / (x. 3),m1) / (x. 0 ),m2) . (x. 0 ) = m2 ) by Lm1, FUNCT_7:34, FUNCT_7:130;

A8: 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 A6;
hence M,((v / (x. 3),m1) / (x. 0 ),m2) / (x. 4),m3 |= (x. 4) '=' (x. 0 ) by A7, ZF_MODEL:12; :: thesis: verum

end;

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 A7, ZF_MODEL:12;
then M,(v / (x. 3),m1) / (x. 4),m3 |= H by A6;
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;

hence M,((v / (x. 3),m1) / (x. 0 ),m2) / (x. 4),m3 |= H <=> ((x. 4) '=' (x. 0 )) by A8, 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