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 = {} )
set m3 = the 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), the Element of M) |= Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))) by A1, ZF_LANG1:71;
then consider m0 being Element of M such that
A3: M,(v / ((x. 3), the Element of M)) / ((x. 0),m0) |= All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))) by ZF_LANG1:73;
let m be Element of M; :: thesis: (def_func' (H,v)) .: m = {}
set u = the Element of (def_func' (H,v)) .: m;
assume (def_func' (H,v)) .: m <> {} ; :: thesis: contradiction
then consider u1 being object such that
A4: u1 in dom (def_func' (H,v)) and
A5: u1 in m and
the Element of (def_func' (H,v)) .: m = (def_func' (H,v)) . u1 by FUNCT_1:def 6;
set f = (v / ((x. 3), the Element of M)) / ((x. 0),m0);
reconsider u1 = u1 as Element of M by A4;

A6: now :: thesis: for m4 being Element of M holds
( M,(v / ((x. 3), the Element of M)) / ((x. 0),m0) |= H iff m4 = m0 )

let m4 be Element of M; :: thesis: ( M,(v / ((x. 3), the Element of M)) / ((x. 0),m0) |= H iff m4 = m0 )
M,((v / ((x. 3), the Element of M)) / ((x. 0),m0)) / ((x. 4),m4) |= H <=> ((x. 4) '=' (x. 0)) by A3, ZF_LANG1:71;
then ( M,((v / ((x. 3), the Element of M)) / ((x. 0),m0)) / ((x. 4),m4) |= H iff M,((v / ((x. 3), the Element of M)) / ((x. 0),m0)) / ((x. 4),m4) |= (x. 4) '=' (x. 0) ) by ZF_MODEL:19;
then A7: ( M,(v / ((x. 3), the Element of M)) / ((x. 0),m0) |= H iff (((v / ((x. 3), the Element of M)) / ((x. 0),m0)) / ((x. 4),m4)) . (x. 4) = (((v / ((x. 3), the Element of M)) / ((x. 0),m0)) / ((x. 4),m4)) . (x. 0) ) by A2, ZFMODEL2:9, ZF_MODEL:12;
( (((v / ((x. 3), the Element of M)) / ((x. 0),m0)) / ((x. 4),m4)) . (x. 4) = m4 & ((v / ((x. 3), the Element of M)) / ((x. 0),m0)) . (x. 0) = m0 ) by FUNCT_7:128;
hence ( M,(v / ((x. 3), the Element of M)) / ((x. 0),m0) |= H iff m4 = m0 ) by A7, FUNCT_7:32, ZF_LANG1:76; :: thesis: verum

end;

then M,(v / ((x. 3), the Element of M)) / ((x. 0),m0) |= H ;
then A: ( u1 = m0 & m = m0 ) by A6;
reconsider uu1 = u1 as set ;
not uu1 in uu1 ;
hence contradiction by A5, A; :: thesis: verum