for p being ZF-formula
for x, y, z being Variable holds
( Ex (x,y,z,p) is existential & bound_in (Ex (x,y,z,p)) = x & the_scope_of (Ex (x,y,z,p)) = Ex (y,z,p) ) by Th9;