Theorem brelg

Description: Two things in a binary relation belong to the relation's domain. (Contributed by Thierry Arnoux, 29-Aug-2017)

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

Proof

Step	Hyp	Ref	Expression
1		ssbr	$$⊢R\subseteq C\times D\to \left(ARB\to A\left(C\times D\right)B\right)$$
2	1	imp	$$⊢\left(R\subseteq C\times D\wedge ARB\right)\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	$$⊢\left(R\subseteq C\times D\wedge ARB\right)\to \left(A\in C\wedge B\in D\right)$$