let p be ZF-formula; :: thesis: for x being Variable holds
( bound_in (Ex x,p) = x & the_scope_of (Ex x,p) = p )
let x be Variable; :: thesis: ( bound_in (Ex x,p) = x & the_scope_of (Ex x,p) = p )
Ex x,p is existential by ZF_LANG:22;
then Ex x,p = Ex (bound_in (Ex x,p)),(the_scope_of (Ex x,p)) by ZF_LANG:63;
hence ( bound_in (Ex x,p) = x & the_scope_of (Ex x,p) = p ) by ZF_LANG:51; :: thesis: verum