theorem Th10: :: ZFMODEL2:10

for M being non empty set
for H being ZF-formula
for v being Function of VAR,M st not x. 0 in Free H & M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) holds
for m1, m2 being Element of M holds
( (def_func' (H,v)) . m1 = m2 iff M,(v / ((x. 3),m1)) / ((x. 4),m2) |= H )