let x, y be Variable; 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 ; 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; ( not x in variables_in H implies ( M |= H / y,x iff M |= H ) )
assume A1:
not x in variables_in H
; ( M |= H / y,x iff M |= H )
thus
( M |= H / y,x implies M |= H )
( M |= H implies M |= H / y,x )proof
assume A2:
for
v being
Function of
VAR ,
M holds
M,
v |= H / y,
x
;
ZF_MODEL:def 5 M |= H
let v be
Function of
VAR ,
M;
ZF_MODEL:def 5 M,v |= H
A3:
(v / x,(v . y)) . x = v . y
by FUNCT_7:130;
M,
v / x,
(v . y) |= H / y,
x
by A2;
then
M,
(v / x,(v . y)) / y,
(v . y) |= H
by A1, A3, Th13;
then A4:
M,
((v / x,(v . y)) / y,(v . y)) / x,
(v . x) |= H
by A1, Th6;
(
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:35;
then
(
M,
v / x,
(v . x) |= H or
M,
(v / y,(v . y)) / x,
(v . x) |= H )
by FUNCT_7:36;
then
M,
v / x,
(v . x) |= H
by FUNCT_7:37;
hence
M,
v |= H
by FUNCT_7:37;
verum
end;
assume A5:
for v being Function of VAR ,M holds M,v |= H
; ZF_MODEL:def 5 M |= H / y,x
let v be Function of VAR ,M; ZF_MODEL:def 5 M,v |= H / y,x
M,v / y,(v . x) |= H
by A5;
hence
M,v |= H / y,x
by A1, Th13; verum