let H be ZF-formula; :: thesis: 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; :: thesis: 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 ; :: thesis: 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; :: thesis: ( 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 ) :: thesis: ( 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) ; :: thesis: 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 ; :: thesis: M,v / (x,(v9 . x)) |= H
thus M,v / (x,(v9 . x)) |= H by A1, FUNCT_7:129; :: thesis: verum

end;

given m being Element of M such that A2: M,v / (x,m) |= H ; :: thesis: M,v |= Ex (x,H)

now :: thesis: ex v9 being Function of VAR,M st
( ( for y being Variable st v9 . y <> v . y holds
x = y ) & M,v9 |= H )

take v9 = v / (x,m); :: thesis: ( ( for y being Variable st v9 . y <> v . y holds
x = y ) & M,v9 |= H )
thus for y being Variable st v9 . y <> v . y holds
x = y by FUNCT_7:32; :: thesis: M,v9 |= H
thus M,v9 |= H by A2; :: thesis: verum

end;

hence M,v |= Ex (x,H) by ZF_MODEL:20; :: thesis: verum