theorem Th19: :: ZFMODEL2:19

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