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	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑅 ↾ 𝑋 ) → 𝐴 ∈ 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		elin	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑅 ∩ ( 𝑋 × V ) ) ↔ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑅 ∧ ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑋 × V ) ) )
2		opelxp1	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑋 × V ) → 𝐴 ∈ 𝑋 )
3	1 2	simplbiim	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑅 ∩ ( 𝑋 × V ) ) → 𝐴 ∈ 𝑋 )
4		df-res	⊢ ( 𝑅 ↾ 𝑋 ) = ( 𝑅 ∩ ( 𝑋 × V ) )
5	3 4	eleq2s	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑅 ↾ 𝑋 ) → 𝐴 ∈ 𝑋 )