let H be ZF-formula; :: thesis: for M being non empty set
for v being Function of VAR,M st M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) & not x. 4 in Free H holds
for m being Element of M holds (def_func' (H,v)) .: m = {}
let M be non empty set ; :: thesis: for v being Function of VAR,M st M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) & not x. 4 in Free H holds
for m being Element of M holds (def_func' (H,v)) .: m = {}
let v be Function of VAR,M; :: thesis: ( M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) & not x. 4 in Free H implies for m being Element of M holds (def_func' (H,v)) .: m = {} )
consider m3 being Element of M;
assume that
A1: M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) and
A2: not x. 4 in Free H ; :: thesis: for m being Element of M holds (def_func' (H,v)) .: m = {}
M,v / ((x. 3),m3) |= Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))) by A1, ZF_LANG1:80;
then consider m0 being Element of M such that
A3: M,(v / ((x. 3),m3)) / ((x. 0),m0) |= All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))) by ZF_LANG1:82;
let m be Element of M; :: thesis: (def_func' (H,v)) .: m = {}
consider u being Element of (def_func' (H,v)) .: m;
assume (def_func' (H,v)) .: m <> {} ; :: thesis: contradiction
then consider u1 being set such that
A4: u1 in dom (def_func' (H,v)) and
A5: u1 in m and
u = (def_func' (H,v)) . u1 by FUNCT_1:def 12;
set f = (v / ((x. 3),m3)) / ((x. 0),m0);
reconsider u1 = u1 as Element of M by A4;

A6: now

let m4 be Element of M; :: thesis: ( M,(v / ((x. 3),m3)) / ((x. 0),m0) |= H iff m4 = m0 )
M,((v / ((x. 3),m3)) / ((x. 0),m0)) / ((x. 4),m4) |= H <=> ((x. 4) '=' (x. 0)) by A3, ZF_LANG1:80;
then ( M,((v / ((x. 3),m3)) / ((x. 0),m0)) / ((x. 4),m4) |= H iff M,((v / ((x. 3),m3)) / ((x. 0),m0)) / ((x. 4),m4) |= (x. 4) '=' (x. 0) ) by ZF_MODEL:19;
then A7: ( M,(v / ((x. 3),m3)) / ((x. 0),m0) |= H iff (((v / ((x. 3),m3)) / ((x. 0),m0)) / ((x. 4),m4)) . (x. 4) = (((v / ((x. 3),m3)) / ((x. 0),m0)) / ((x. 4),m4)) . (x. 0) ) by A2, ZFMODEL2:10, ZF_MODEL:12;
( (((v / ((x. 3),m3)) / ((x. 0),m0)) / ((x. 4),m4)) . (x. 4) = m4 & ((v / ((x. 3),m3)) / ((x. 0),m0)) . (x. 0) = m0 ) by FUNCT_7:130;
hence ( M,(v / ((x. 3),m3)) / ((x. 0),m0) |= H iff m4 = m0 ) by A7, FUNCT_7:34, ZF_LANG1:86; :: thesis: verum

end;

then M,(v / ((x. 3),m3)) / ((x. 0),m0) |= H ;
then ( u1 = m0 & m = m0 ) by A6;
hence contradiction by A5; :: thesis: verum