theorem :: ZF_LANG1:132

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