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:151;
then A1: ( x in Free H implies x in variables_in H ) ;
v / (x,(v . x)) = v by FUNCT_7:35;
hence ( not x in variables_in H implies ( M,v |= H iff M,v |= All (x,H) ) ) by A1, ZFMODEL1:10, ZF_LANG1:71; :: thesis: verum