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 ) :: 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 )

proof

assume A1: for v being Function of VAR ,M holds M,v |= Ex x,H ; :: according to ZF_MODEL:def 5 :: thesis: for v being Function of VAR ,M ex m being Element of M st M,v / x,m |= H
let v be Function of VAR ,M; :: thesis: ex m being Element of M st M,v / x,m |= H
M,v |= Ex x,H by A1;
hence ex m being Element of M st M,v / x,m |= H by Th82; :: thesis: verum

end;

assume A2: 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 A2;
hence M,v |= Ex x,H by Th82; :: thesis: verum