theorem Th11: :: ZFMODEL2:11

for M being non empty set
for H being ZF-formula
for v being Function of VAR,M st Free H c= {(x. 3),(x. 4)} & M |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) holds
def_func' (H,v) = def_func (H,M)