let G1, G2, H1, H2 be ZF-formula; :: thesis: for x, y being Variable holds
( G1 '&' G2 = (H1 '&' H2) / (x,y) iff ( G1 = H1 / (x,y) & G2 = H2 / (x,y) ) )
let x, y be Variable; :: thesis: ( G1 '&' G2 = (H1 '&' H2) / (x,y) iff ( G1 = H1 / (x,y) & G2 = H2 / (x,y) ) )
thus ( G1 '&' G2 = (H1 '&' H2) / (x,y) implies ( G1 = H1 / (x,y) & G2 = H2 / (x,y) ) ) :: thesis: ( G1 = H1 / (x,y) & G2 = H2 / (x,y) implies G1 '&' G2 = (H1 '&' H2) / (x,y) )
proof
assume G1 '&' G2 = (H1 '&' H2) / (x,y) ; :: thesis: ( G1 = H1 / (x,y) & G2 = H2 / (x,y) )
then G1 '&' G2 = (H1 / (x,y)) '&' (H2 / (x,y)) by Lm1;
hence ( G1 = H1 / (x,y) & G2 = H2 / (x,y) ) by ZF_LANG:30; :: thesis: verum
end;
thus ( G1 = H1 / (x,y) & G2 = H2 / (x,y) implies G1 '&' G2 = (H1 '&' H2) / (x,y) ) by Lm1; :: thesis: verum