let H be ZF-formula; :: thesis: for x being Variable
for M being non empty set
for m being Element of M
for v being Function of VAR ,M holds
( M,v |= Ex x,H iff M,v / x,m |= Ex x,H )
let x be Variable; :: thesis: for M being non empty set
for m being Element of M
for v being Function of VAR ,M holds
( M,v |= Ex x,H iff M,v / x,m |= Ex x,H )
let M be non empty set ; :: thesis: for m being Element of M
for v being Function of VAR ,M holds
( M,v |= Ex x,H iff M,v / x,m |= Ex x,H )
let m be Element of M; :: thesis: for v being Function of VAR ,M holds
( M,v |= Ex x,H iff M,v / x,m |= Ex x,H )
let v be Function of VAR ,M; :: thesis: ( M,v |= Ex x,H iff M,v / x,m |= Ex x,H )
A1: (v / x,m) / x,(v . x) =
v / x,(v . x)
by FUNCT_7:36
.=
v
by FUNCT_7:37
;
for v being Function of VAR ,M
for m being Element of M st M,v |= Ex x,H holds
M,v / x,m |= Ex x,H
proof
let v be
Function of
VAR ,
M;
:: thesis: for m being Element of M st M,v |= Ex x,H holds
M,v / x,m |= Ex x,Hlet m be
Element of
M;
:: thesis: ( M,v |= Ex x,H implies M,v / x,m |= Ex x,H )
assume
M,
v |= Ex x,
H
;
:: thesis: M,v / x,m |= Ex x,H
then consider m' being
Element of
M such that A2:
M,
v / x,
m' |= H
by Th82;
(v / x,m) / x,
m' = v / x,
m'
by FUNCT_7:36;
hence
M,
v / x,
m |= Ex x,
H
by A2, Th82;
:: thesis: verum
end;
hence
( M,v |= Ex x,H iff M,v / x,m |= Ex x,H )
by A1; :: thesis: verum