theorem Th4: :: ZFMODEL2:4

for x being Variable
for M being non empty set
for H being ZF-formula
for v being Function of VAR,M st not x in variables_in H holds
( M,v |= H iff M,v |= All (x,H) )