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 that
A1: not x in variables_in H and
A2: M,v |= H ; :: thesis: M,v / (x,(v . y)) |= H / (y,x)
A3: (v / (x,(v . y))) . x = v . y by FUNCT_7:128;
( x = y or x <> y ) ;
then A4: (v / (x,(v . y))) / (y,(v . y)) = (v / (y,(v . y))) / (x,(v . y)) by FUNCT_7:33;
A5: v / (y,(v . y)) = v by FUNCT_7:35;
M,v / (x,(v . y)) |= H by A1, A2, Th5;
hence M,v / (x,(v . y)) |= H / (y,x) by A1, A4, A3, A5, Th12; :: thesis: verum