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:63;
hence ( M,v |= H iff ex m being Element of M st M,v / (bound_in H),m |= the_scope_of H ) by Th82; :: thesis: verum