Metamath Proof Explorer


Theorem brinxp2

Description: Intersection of binary relation with Cartesian product. (Contributed by NM, 3-Mar-2007) (Revised by Mario Carneiro, 26-Apr-2015) Group conjuncts and avoid df-3an . (Revised by Peter Mazsa, 18-Sep-2022)

Ref Expression
Assertion brinxp2
|- ( C ( R i^i ( A X. B ) ) D <-> ( ( C e. A /\ D e. B ) /\ C R D ) )

Proof

Step Hyp Ref Expression
1 brin
 |-  ( C ( R i^i ( A X. B ) ) D <-> ( C R D /\ C ( A X. B ) D ) )
2 ancom
 |-  ( ( C R D /\ C ( A X. B ) D ) <-> ( C ( A X. B ) D /\ C R D ) )
3 brxp
 |-  ( C ( A X. B ) D <-> ( C e. A /\ D e. B ) )
4 3 anbi1i
 |-  ( ( C ( A X. B ) D /\ C R D ) <-> ( ( C e. A /\ D e. B ) /\ C R D ) )
5 1 2 4 3bitri
 |-  ( C ( R i^i ( A X. B ) ) D <-> ( ( C e. A /\ D e. B ) /\ C R D ) )