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:130;
( x = y or x <> y ) ;
then A4: (v / x,(v . y)) / y,(v . y) = (v / y,(v . y)) / x,(v . y) by FUNCT_7:35;
A5: v / y,(v . y) = v by FUNCT_7:37;
M,v / x,(v . y) |= H by A1, A2, Th6;
hence M,v / x,(v . y) |= H / y,x by A1, A4, A3, A5, Th13; :: thesis: verum