theorem :: ZF_LANG1:93

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