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, Th164, Th165;
hence H / (x,y) is existential ; :: 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;
then H is negative by Th168;
then consider H1 being ZF-formula such that
A4: H = 'not' H1 ;
( bound_in H1 = x or bound_in H1 <> x ) ;
then consider s being Variable such that
A5: ( ( bound_in H1 = x & s = y ) or ( bound_in H1 <> x & s = bound_in H1 ) ) ;
A6: H1 / (x,y) = All (z,('not' G)) by A3, A4, Th156;
then H1 / (x,y) is universal ;
then H1 is universal by Th170;
then A7: H1 = All ((bound_in H1),(the_scope_of H1)) by ZF_LANG:44;
then All (z,('not' G)) = All (s,((the_scope_of H1) / (x,y))) by A6, A5, Th159, Th160;
then 'not' G = (the_scope_of H1) / (x,y) by ZF_LANG:3;
then (the_scope_of H1) / (x,y) is negative ;
then the_scope_of H1 is negative by Th168;
then H = Ex ((bound_in H1),(the_argument_of (the_scope_of H1))) by A4, A7, ZF_LANG:def 30;
hence H is existential ; :: thesis: verum