Theorem brinxp

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

	Ref	Expression
Assertion	brinxp	$$⊢\left(A\in C\wedge B\in D\right)\to \left(ARB\leftrightarrow A\left(R\cap \left(C\times D\right)\right)B\right)$$

Proof

Step	Hyp	Ref	Expression
1		brinxp2	$$⊢A\left(R\cap \left(C\times D\right)\right)B\leftrightarrow \left(\left(A\in C\wedge B\in D\right)\wedge ARB\right)$$
2	1	baibr	$$⊢\left(A\in C\wedge B\in D\right)\to \left(ARB\leftrightarrow A\left(R\cap \left(C\times D\right)\right)B\right)$$