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) )

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

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 A5:
for v being Function of VAR,M holds M,v |= H
; :: according to ZF_MODEL:def 5 :: thesis: M |= H / (y,x)
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;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

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