# Metamath Proof Explorer

## Theorem brinxp2

Description: Intersection with cross product binary relation. (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}\left({R}\cap \left({A}×{B}\right)\right){D}↔\left(\left({C}\in {A}\wedge {D}\in {B}\right)\wedge {C}{R}{D}\right)$

### Proof

Step Hyp Ref Expression
1 brin ${⊢}{C}\left({R}\cap \left({A}×{B}\right)\right){D}↔\left({C}{R}{D}\wedge {C}\left({A}×{B}\right){D}\right)$
2 ancom ${⊢}\left({C}{R}{D}\wedge {C}\left({A}×{B}\right){D}\right)↔\left({C}\left({A}×{B}\right){D}\wedge {C}{R}{D}\right)$
3 brxp ${⊢}{C}\left({A}×{B}\right){D}↔\left({C}\in {A}\wedge {D}\in {B}\right)$
4 3 anbi1i ${⊢}\left({C}\left({A}×{B}\right){D}\wedge {C}{R}{D}\right)↔\left(\left({C}\in {A}\wedge {D}\in {B}\right)\wedge {C}{R}{D}\right)$
5 1 2 4 3bitri ${⊢}{C}\left({R}\cap \left({A}×{B}\right)\right){D}↔\left(\left({C}\in {A}\wedge {D}\in {B}\right)\wedge {C}{R}{D}\right)$