theorem :: ZF_LANG1:12

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