Metamath Proof Explorer

Theorem brinxp

Description: Intersection of binary relation with Cartesian product. (Contributed by NM, 9-Mar-1997)

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

Proof

Step Hyp Ref Expression
1 brinxp2 
 |-  ( A ( R i^i ( C X. D ) ) B <-> ( ( A e. C /\ B e. D ) /\ A R B ) )
2 1 baibr 
 |-  ( ( A e. C /\ B e. D ) -> ( A R B <-> A ( R i^i ( C X. D ) ) B ) )