Theorem brxp

Description: Binary relation on a Cartesian product. (Contributed by NM, 22-Apr-2004)

	Ref	Expression
Assertion	brxp	$$⊢A\left(C\times D\right)B\leftrightarrow \left(A\in C\wedge B\in D\right)$$

Proof

Step	Hyp	Ref	Expression
1		df-br	$$⊢A\left(C\times D\right)B\leftrightarrow ⟨A,B⟩\in \left(C\times D\right)$$
2		opelxp	$$⊢⟨A,B⟩\in \left(C\times D\right)\leftrightarrow \left(A\in C\wedge B\in D\right)$$
3	1 2	bitri	$$⊢A\left(C\times D\right)B\leftrightarrow \left(A\in C\wedge B\in D\right)$$