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	⊢ ( ( Rel 𝑅 ∧ ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑅 ) → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )

Proof

Step	Hyp	Ref	Expression
1		df-rel	⊢ ( Rel 𝑅 ↔ 𝑅 ⊆ ( V × V ) )
2	1	biimpi	⊢ ( Rel 𝑅 → 𝑅 ⊆ ( V × V ) )
3	2	sselda	⊢ ( ( Rel 𝑅 ∧ ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑅 ) → ⟨ 𝐴 , 𝐵 ⟩ ∈ ( V × V ) )
4		opelxp	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( V × V ) ↔ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )
5	3 4	sylib	⊢ ( ( Rel 𝑅 ∧ ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑅 ) → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )