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 A × B D C A D B C R D

Proof

Step Hyp Ref Expression
1 brin C R A × B D C R D C A × B D
2 ancom C R D C A × B D C A × B D C R D
3 brxp C A × B D C A D B
4 3 anbi1i C A × B D C R D C A D B C R D
5 1 2 4 3bitri C R A × B D C A D B C R D