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

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