theorem :: ZF_LANG1:74

for H being ZF-formula
for x being Variable
for M being non empty set
for m being Element of M
for v being Function of VAR,M holds
( M,v |= Ex (x,H) iff M,v / (x,m) |= Ex (x,H) )