theorem :: ZF_LANG1:131

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