let x, y be Variable; :: thesis: for M being non empty set
for H being ZF-formula st not x in variables_in H holds
( M |= H / (y,x) iff M |= H )
let M be non empty set ; :: thesis: for H being ZF-formula st not x in variables_in H holds
( M |= H / (y,x) iff M |= H )
let H be ZF-formula; :: thesis: ( not x in variables_in H implies ( M |= H / (y,x) iff M |= H ) )
assume A1: not x in variables_in H ; :: thesis: ( M |= H / (y,x) iff M |= H )
thus ( M |= H / (y,x) implies M |= H ) :: thesis: ( M |= H implies M |= H / (y,x) )

proof

assume A2: for v being Function of VAR,M holds M,v |= H / (y,x) ; :: according to ZF_MODEL:def 5 :: thesis: M |= H
let v be Function of VAR,M; :: according to ZF_MODEL:def 5 :: thesis: M,v |= H
A3: (v / (x,(v . y))) . x = v . y by FUNCT_7:128;
M,v / (x,(v . y)) |= H / (y,x) by A2;
then M,(v / (x,(v . y))) / (y,(v . y)) |= H by A1, A3, Th12;
then A4: M,((v / (x,(v . y))) / (y,(v . y))) / (x,(v . x)) |= H by A1, Th5;
( x = y or x <> y ) ;
then ( M,(v / (x,(v . y))) / (x,(v . x)) |= H or M,((v / (y,(v . y))) / (x,(v . y))) / (x,(v . x)) |= H ) by A4, FUNCT_7:33;
then ( M,v / (x,(v . x)) |= H or M,(v / (y,(v . y))) / (x,(v . x)) |= H ) by FUNCT_7:34;
then M,v / (x,(v . x)) |= H by FUNCT_7:35;
hence M,v |= H by FUNCT_7:35; :: thesis: verum

end;

assume A5: for v being Function of VAR,M holds M,v |= H ; :: according to ZF_MODEL:def 5 :: thesis: M |= H / (y,x)
let v be Function of VAR,M; :: according to ZF_MODEL:def 5 :: thesis: M,v |= H / (y,x)
M,v / (y,(v . x)) |= H by A5;
hence M,v |= H / (y,x) by A1, Th12; :: thesis: verum