Theorem bj-opelresdm

Description: If an ordered pair is in a restricted binary relation, then its first component is an element of the restricting class. See also opelres . (Contributed by BJ, 25-Dec-2023)

	Ref	Expression
Assertion	bj-opelresdm	$$⊢⟨A,B⟩\in \left({R\upharpoonright }_X\right)\to A\in X$$

Proof

Step	Hyp	Ref	Expression
1		elin	$$⊢⟨A,B⟩\in \left(R\cap \left(X\times \mathrm{V}\right)\right)\leftrightarrow \left(⟨A,B⟩\in R\wedge ⟨A,B⟩\in \left(X\times \mathrm{V}\right)\right)$$
2		opelxp1	$$⊢⟨A,B⟩\in \left(X\times \mathrm{V}\right)\to A\in X$$
3	1 2	simplbiim	$$⊢⟨A,B⟩\in \left(R\cap \left(X\times \mathrm{V}\right)\right)\to A\in X$$
4		df-res	$$⊢{R\upharpoonright }_X=R\cap \left(X\times \mathrm{V}\right)$$
5	3 4	eleq2s	$$⊢⟨A,B⟩\in \left({R\upharpoonright }_X\right)\to A\in X$$