let H be ZF-formula; :: thesis: for x, y being Variable holds
( H is conjunctive iff H / (x,y) is conjunctive )
let x, y be Variable; :: thesis: ( H is conjunctive iff H / (x,y) is conjunctive )
thus ( H is conjunctive implies H / (x,y) is conjunctive ) :: thesis: ( H / (x,y) is conjunctive implies H is conjunctive )
proof
given H1, H2 being ZF-formula such that A1: H = H1 '&' H2 ; :: according to ZF_LANG:def 13 :: thesis: H / (x,y) is conjunctive
H / (x,y) = (H1 / (x,y)) '&' (H2 / (x,y)) by A1, Th158;
hence H / (x,y) is conjunctive ; :: thesis: verum
end;
assume H / (x,y) is conjunctive ; :: thesis: H is conjunctive
then A2: (H / (x,y)) . 1 = 3 by ZF_LANG:21;
3 <= len H by ZF_LANG:13;
then 1 <= len H by XXREAL_0:2;
then A3: 1 in dom H by FINSEQ_3:25;
y <> 3 by Th135;
then H . 1 <> x by A2, A3, Def3;
then 3 = H . 1 by A2, A3, Def3;
hence H is conjunctive by ZF_LANG:27; :: thesis: verum