Theorem brel

Description: Two things in a binary relation belong to the relation's domain. (Contributed by NM, 17-May-1996) (Revised by Mario Carneiro, 26-Apr-2015)

	Ref	Expression
Hypothesis	brel.1	$$⊢R\subseteq C\times D$$
Assertion	brel	$$⊢ARB\to \left(A\in C\wedge B\in D\right)$$

Proof

Step	Hyp	Ref	Expression
1		brel.1	$$⊢R\subseteq C\times D$$
2	1	ssbri	$$⊢ARB\to A\left(C\times D\right)B$$
3		brxp	$$⊢A\left(C\times D\right)B\leftrightarrow \left(A\in C\wedge B\in D\right)$$
4	2 3	sylib	$$⊢ARB\to \left(A\in C\wedge B\in D\right)$$