let H be ZF-formula; 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 ; 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; ( 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
; ( 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; verum