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:71;
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:73;
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, Th9;
then A4: M,((v / ((x. 3),m1)) / ((x. 0),m2)) / ((x. 4),m3) |= H by FUNCT_7:33, ZF_LANG1:76;
M,((v / ((x. 3),m1)) / ((x. 0),m2)) / ((x. 4),m3) |= H <=> ((x. 4) '=' (x. 0)) by A3, ZF_LANG1:71;
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:128;
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:32, ZF_LANG1:76;
(((v / ((x. 3),m1)) / ((x. 0),m2)) / ((x. 4),m3)) . (x. 4) = m3 by FUNCT_7:128;
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:71;
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:32, ZF_LANG1:76;
A10: ((v / ((x. 3),m1)) / ((x. 0),m3)) . (x. 0) = m3 by FUNCT_7:128;
(((v / ((x. 3),m1)) / ((x. 0),m3)) / ((x. 4),m3)) . (x. 4) = m3 by FUNCT_7:128;
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:33, ZF_LANG1:76;
hence M,(v / ((x. 3),m1)) / ((x. 4),m3) |= H by A1, Th9; :: 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 :: thesis: for m1 being Element of M holds M,v / ((x. 3),m1) |= Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0))))))

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 :: thesis: for m3 being Element of M holds M,((v / ((x. 3),m1)) / ((x. 0),m2)) / ((x. 4),m3) |= H <=> ((x. 4) '=' (x. 0))

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:32, ZF_LANG1:76;
A14: ((v / ((x. 3),m1)) / ((x. 0),m2)) . (x. 0) = m2 by FUNCT_7:128;
A15: (((v / ((x. 3),m1)) / ((x. 0),m2)) / ((x. 4),m3)) . (x. 4) = m3 by FUNCT_7:128;

A16: now :: thesis: ( M,((v / ((x. 3),m1)) / ((x. 0),m2)) / ((x. 4),m3) |= (x. 4) '=' (x. 0) implies M,((v / ((x. 3),m1)) / ((x. 0),m2)) / ((x. 4),m3) |= H )

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, Th9;
hence M,((v / ((x. 3),m1)) / ((x. 0),m2)) / ((x. 4),m3) |= H by FUNCT_7:33, ZF_LANG1:76; :: thesis: verum

end;

now :: thesis: ( M,((v / ((x. 3),m1)) / ((x. 0),m2)) / ((x. 4),m3) |= H implies M,((v / ((x. 3),m1)) / ((x. 0),m2)) / ((x. 4),m3) |= (x. 4) '=' (x. 0) )

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:33, ZF_LANG1:76;
then M,(v / ((x. 3),m1)) / ((x. 4),m3) |= H by A1, Th9;
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:71;
hence M,v / ((x. 3),m1) |= Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))) by ZF_LANG1:73; :: thesis: verum

end;

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