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 )
set G = H / (x,y);
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, Th162;
hence H / (x,y) is conditional ; :: thesis: verum
end;
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;
then H is negative by Th168;
then consider H9 being ZF-formula such that
A3: H = 'not' H9 ;
A4: G1 '&' ('not' G2) = H9 / (x,y) by A2, A3, Th156;
then H9 / (x,y) is conjunctive ;
then H9 is conjunctive by Th169;
then consider H1, H2 being ZF-formula such that
A5: H9 = H1 '&' H2 ;
'not' G2 = H2 / (x,y) by A4, A5, Th158;
then H2 / (x,y) is negative ;
then H2 is negative by Th168;
then consider p2 being ZF-formula such that
A6: H2 = 'not' p2 ;
H = H1 => p2 by A3, A5, A6;
hence H is conditional ; :: thesis: verum