let H be ZF-formula; :: thesis: for x being Variable
for M being non empty set holds
( M |= Ex (x,H) iff for v being Function of VAR,M ex m being Element of M st M,v / (x,m) |= H )
let x be Variable; :: thesis: for M being non empty set holds
( M |= Ex (x,H) iff for v being Function of VAR,M ex m being Element of M st M,v / (x,m) |= H )
let M be non empty set ; :: thesis: ( M |= Ex (x,H) iff for v being Function of VAR,M ex m being Element of M st M,v / (x,m) |= H )
thus ( M |= Ex (x,H) implies for v being Function of VAR,M ex m being Element of M st M,v / (x,m) |= H ) by Th73; :: thesis: ( ( for v being Function of VAR,M ex m being Element of M st M,v / (x,m) |= H ) implies M |= Ex (x,H) )
assume A1: for v being Function of VAR,M ex m being Element of M st M,v / (x,m) |= H ; :: thesis: M |= Ex (x,H)
let v be Function of VAR,M; :: according to ZF_MODEL:def 5 :: thesis: M,v |= Ex (x,H)
ex m being Element of M st M,v / (x,m) |= H by A1;
hence M,v |= Ex (x,H) by Th73; :: thesis: verum