let H be ZF-formula; for x being Variable
for M being non empty set
for v being Function of VAR,M holds
( M,v |= Ex (x,H) iff ex m being Element of M st M,v / (x,m) |= H )
let x be Variable; for M being non empty set
for v being Function of VAR,M holds
( M,v |= Ex (x,H) iff ex m being Element of M st M,v / (x,m) |= H )
let M be non empty set ; for v being Function of VAR,M holds
( M,v |= Ex (x,H) iff ex m being Element of M st M,v / (x,m) |= H )
let v be Function of VAR,M; ( M,v |= Ex (x,H) iff ex m being Element of M st M,v / (x,m) |= H )
thus
( M,v |= Ex (x,H) implies ex m being Element of M st M,v / (x,m) |= H )
( ex m being Element of M st M,v / (x,m) |= H implies M,v |= Ex (x,H) )proof
assume
M,
v |= Ex (
x,
H)
;
ex m being Element of M st M,v / (x,m) |= H
then consider v9 being
Function of
VAR,
M such that A1:
( ( for
y being
Variable st
v9 . y <> v . y holds
x = y ) &
M,
v9 |= H )
by ZF_MODEL:20;
take
v9 . x
;
M,v / (x,(v9 . x)) |= H
thus
M,
v / (
x,
(v9 . x))
|= H
by A1, FUNCT_7:129;
verum
end;
given m being Element of M such that A2:
M,v / (x,m) |= H
; M,v |= Ex (x,H)
hence
M,v |= Ex (x,H)
by ZF_MODEL:20; verum