let x be Variable; :: thesis: 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 )
let M be non empty set ; :: thesis: 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 )
let H be ZF-formula; :: thesis: for v being Function of VAR ,M st not x in variables_in H holds
( M,v |= H iff M,v |= All x,H )
let v be Function of VAR ,M; :: thesis: ( not x in variables_in H implies ( M,v |= H iff M,v |= All x,H ) )
Free H c= variables_in H by ZF_LANG1:164;
then ( ( x in Free H implies x in variables_in H ) & v / x,(v . x) = v ) by FUNCT_7:37;
hence ( not x in variables_in H implies ( M,v |= H iff M,v |= All x,H ) ) by ZFMODEL1:10, ZF_LANG1:80; :: thesis: verum