let H be ZF-formula; :: thesis: for x, y being Variable holds
( H is existential iff H / x,y is existential )
let x, y be Variable; :: thesis: ( H is existential iff H / x,y is existential )
thus ( H is existential implies H / x,y is existential ) :: thesis: ( H / x,y is existential implies H is existential )

proof

given z being Variable, H1 being ZF-formula such that A1: H = Ex z,H1 ; :: according to ZF_LANG:def 23 :: thesis: H / x,y is existential
( z = x or z <> x ) ;
then consider s being Variable such that
A2: ( ( z = x & s = y ) or ( z <> x & s = z ) ) ;
H / x,y = Ex s,(H1 / x,y) by A1, A2, Th178, Th179;
hence H / x,y is existential by ZF_LANG:22; :: thesis: verum

end;

given z being Variable, G being ZF-formula such that A3: H / x,y = Ex z,G ; :: according to ZF_LANG:def 23 :: thesis: H is existential
H / x,y is negative by A3, ZF_LANG:16;
then H is negative by Th182;
then consider H1 being ZF-formula such that
A4: H = 'not' H1 by ZF_LANG:16;
A5: H1 / x,y = All z,('not' G) by A3, A4, Th170;
( bound_in H1 = x or bound_in H1 <> x ) ;
then consider s being Variable such that
A6: ( ( bound_in H1 = x & s = y ) or ( bound_in H1 <> x & s = bound_in H1 ) ) ;
H1 / x,y is universal by A5, ZF_LANG:16;
then H1 is universal by Th184;
then A7: H1 = All (bound_in H1),(the_scope_of H1) by ZF_LANG:62;
then All z,('not' G) = All s,((the_scope_of H1) / x,y) by A5, A6, Th173, Th174;
then 'not' G = (the_scope_of H1) / x,y by ZF_LANG:12;
then (the_scope_of H1) / x,y is negative by ZF_LANG:16;
then the_scope_of H1 is negative by Th182;
then H = Ex (bound_in H1),(the_argument_of (the_scope_of H1)) by A4, A7, ZF_LANG:def 30;
hence H is existential by ZF_LANG:22; :: thesis: verum