theorem :: ZF_LANG:45

for H being ZF-formula st H is existential holds
H = Ex ((bound_in H),(the_scope_of H))