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

proof

given H1, H2 being ZF-formula such that A1: H = H1 => H2 ; :: according to ZF_LANG:def 21 :: thesis: H / x,y is conditional
H / x,y = (H1 / x,y) => (H2 / x,y) by A1, Th176;
hence H / x,y is conditional by ZF_LANG:22; :: thesis: verum

end;

set G = H / x,y;
given G1, G2 being ZF-formula such that A2: H / x,y = G1 => G2 ; :: according to ZF_LANG:def 21 :: thesis: H is conditional
H / x,y is negative by A2, ZF_LANG:16;
then H is negative by Th182;
then consider H' being ZF-formula such that
A3: H = 'not' H' by ZF_LANG:16;
A4: G1 '&' ('not' G2) = H' / x,y by A2, A3, Th170;
then H' / x,y is conjunctive by ZF_LANG:16;
then H' is conjunctive by Th183;
then consider H1, H2 being ZF-formula such that
A5: H' = H1 '&' H2 by ZF_LANG:16;
( G1 = H1 / x,y & 'not' G2 = H2 / x,y ) by A4, A5, Th172;
then H2 / x,y is negative by ZF_LANG:16;
then H2 is negative by Th182;
then consider p2 being ZF-formula such that
A6: H2 = 'not' p2 by ZF_LANG:16;
H = H1 => p2 by A3, A5, A6;
hence H is conditional by ZF_LANG:22; :: thesis: verum