theorem :: ZF_LANG1:133

for H1, H2 being ZF-formula
for x being Variable
for M being non empty set st M |= (Ex (x,H1)) => H2 holds
M |= H1 => H2