theorem :: ZF_LANG1:98

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