theorem :: ZF_LANG1:127

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