theorem :: ZF_LANG1:29

for H being ZF-formula st H is existential holds
( bound_in H = bound_in (the_argument_of H) & the_scope_of H = the_argument_of (the_scope_of (the_argument_of H)) )