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 ( 𝐶 ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) 𝐷 ↔ ( ( 𝐶𝐴𝐷𝐵 ) ∧ 𝐶 𝑅 𝐷 ) )

Proof

Step Hyp Ref Expression
1 brin ( 𝐶 ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) 𝐷 ↔ ( 𝐶 𝑅 𝐷𝐶 ( 𝐴 × 𝐵 ) 𝐷 ) )
2 ancom ( ( 𝐶 𝑅 𝐷𝐶 ( 𝐴 × 𝐵 ) 𝐷 ) ↔ ( 𝐶 ( 𝐴 × 𝐵 ) 𝐷𝐶 𝑅 𝐷 ) )
3 brxp ( 𝐶 ( 𝐴 × 𝐵 ) 𝐷 ↔ ( 𝐶𝐴𝐷𝐵 ) )
4 3 anbi1i ( ( 𝐶 ( 𝐴 × 𝐵 ) 𝐷𝐶 𝑅 𝐷 ) ↔ ( ( 𝐶𝐴𝐷𝐵 ) ∧ 𝐶 𝑅 𝐷 ) )
5 1 2 4 3bitri ( 𝐶 ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) 𝐷 ↔ ( ( 𝐶𝐴𝐷𝐵 ) ∧ 𝐶 𝑅 𝐷 ) )