let H be ZF-formula; :: thesis: for M being non empty set
for v being Function of VAR,M st H is existential holds
( M,v |= H iff ex m being Element of M st M,v / ((bound_in H),m) |= the_scope_of H )
let M be non empty set ; :: thesis: for v being Function of VAR,M st H is existential holds
( M,v |= H iff ex m being Element of M st M,v / ((bound_in H),m) |= the_scope_of H )
let v be Function of VAR,M; :: thesis: ( H is existential implies ( M,v |= H iff ex m being Element of M st M,v / ((bound_in H),m) |= the_scope_of H ) )
assume H is existential ; :: thesis: ( M,v |= H iff ex m being Element of M st M,v / ((bound_in H),m) |= the_scope_of H )
then H = Ex ((bound_in H),(the_scope_of H)) by ZF_LANG:45;
hence ( M,v |= H iff ex m being Element of M st M,v / ((bound_in H),m) |= the_scope_of H ) by Th73; :: thesis: verum