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

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

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 A11:
for m1 being Element of M ex m2 being Element of M st
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 )

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;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
m3 = m2
; :: thesis: M,(v / ((x. 3),m1)) / ((x. 4),m3) |= H
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;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

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

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

hence
M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0))))))))
by ZF_LANG1:71; :: thesis: verumlet 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;

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

end;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))

then
M,(v / ((x. 3),m1)) / ((x. 0),m2) |= All ((x. 4),(H <=> ((x. 4) '=' (x. 0))))
by ZF_LANG1:71;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;

end;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;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

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

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

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