let x, y 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 & M,v |= H holds
M,v / x,(v . y) |= H / y,x
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 & M,v |= H holds
M,v / x,(v . y) |= H / y,x
let H be ZF-formula; :: thesis: for v being Function of VAR ,M st not x in variables_in H & M,v |= H holds
M,v / x,(v . y) |= H / y,x
let v be Function of VAR ,M; :: thesis: ( not x in variables_in H & M,v |= H implies M,v / x,(v . y) |= H / y,x )
assume A1: ( not x in variables_in H & M,v |= H ) ; :: thesis: M,v / x,(v . y) |= H / y,x
( x = y or x <> y ) ;
then ( (v / x,(v . y)) / y,(v . y) = (v / y,(v . y)) / x,(v . y) & (v / x,(v . y)) . x = v . y & v / y,(v . y) = v & M,v / x,(v . y) |= H ) by A1, Th6, FUNCT_7:37, FUNCT_7:35, FUNCT_7:130;
hence M,v / x,(v . y) |= H / y,x by A1, Th13; :: thesis: verum