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 )proof
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
(
M,
v / x,
(v . y) |= H / y,
x &
(v / x,(v . y)) . x = v . y )
by A2, FUNCT_7:130;
then
M,
(v / x,(v . y)) / y,
(v . y) |= H
by A1, Th13;
then
(
M,
((v / x,(v . y)) / y,(v . y)) / x,
(v . x) |= H & (
x = y or
x <> y ) )
by A1, Th6;
then
(
M,
(v / x,(v . y)) / x,
(v . x) |= H or
M,
((v / y,(v . y)) / x,(v . y)) / x,
(v . x) |= H )
by 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;
:: thesis: verum
end;
assume A3:
for v being Function of VAR ,M holds M,v |= H
; :: according to ZF_MODEL:def 5 :: thesis: 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 A3;
hence
M,v |= H / y,x
by A1, Th13; :: thesis: verum