Theorem bj-opelrelex

Description: The coordinates of an ordered pair that belongs to a relation are sets. TODO: Slightly shorter than brrelex12 , which could be proved from it. (Contributed by BJ, 27-Dec-2023)

	Ref	Expression
Assertion	bj-opelrelex	$$⊢\left(\mathrm{Rel}R\wedge ⟨A,B⟩\in R\right)\to \left(A\in \mathrm{V}\wedge B\in \mathrm{V}\right)$$

Proof

Step	Hyp	Ref	Expression
1		df-rel	$$⊢\mathrm{Rel}R\leftrightarrow R\subseteq \mathrm{V}\times \mathrm{V}$$
2	1	biimpi	$$⊢\mathrm{Rel}R\to R\subseteq \mathrm{V}\times \mathrm{V}$$
3	2	sselda	$$⊢\left(\mathrm{Rel}R\wedge ⟨A,B⟩\in R\right)\to ⟨A,B⟩\in \left(\mathrm{V}\times \mathrm{V}\right)$$
4		opelxp	$$⊢⟨A,B⟩\in \left(\mathrm{V}\times \mathrm{V}\right)\leftrightarrow \left(A\in \mathrm{V}\wedge B\in \mathrm{V}\right)$$
5	3 4	sylib	$$⊢\left(\mathrm{Rel}R\wedge ⟨A,B⟩\in R\right)\to \left(A\in \mathrm{V}\wedge B\in \mathrm{V}\right)$$