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

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