let H be ZF-formula; :: thesis: for x, y being Variable st H is existential holds
( the_scope_of (H / x,y) = (the_scope_of H) / x,y & ( bound_in H = x implies bound_in (H / x,y) = y ) & ( bound_in H <> x implies bound_in (H / x,y) = bound_in H ) )
let x, y be Variable; :: thesis: ( H is existential implies ( the_scope_of (H / x,y) = (the_scope_of H) / x,y & ( bound_in H = x implies bound_in (H / x,y) = y ) & ( bound_in H <> x implies bound_in (H / x,y) = bound_in H ) ) )
assume H is existential ; :: thesis: ( the_scope_of (H / x,y) = (the_scope_of H) / x,y & ( bound_in H = x implies bound_in (H / x,y) = y ) & ( bound_in H <> x implies bound_in (H / x,y) = bound_in H ) )
then ( H / x,y is existential & H = Ex (bound_in H),(the_scope_of H) ) by Th191, ZF_LANG:63;
then ( H / x,y = Ex (bound_in (H / x,y)),(the_scope_of (H / x,y)) & ( bound_in H = x implies H / x,y = Ex y,((the_scope_of H) / x,y) ) & ( bound_in H <> x implies H / x,y = Ex (bound_in H),((the_scope_of H) / x,y) ) ) by Th178, Th179, ZF_LANG:63;
hence ( the_scope_of (H / x,y) = (the_scope_of H) / x,y & ( bound_in H = x implies bound_in (H / x,y) = y ) & ( bound_in H <> x implies bound_in (H / x,y) = bound_in H ) ) by ZF_LANG:51; :: thesis: verum