theorem :: ZF_LANG1:129

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