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: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;
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, Th12; verum