Theorem elrel

Description: A member of a relation is an ordered pair. (Contributed by NM, 17-Sep-2006)

	Ref	Expression
Assertion	elrel	⊢ ( ( Rel 𝑅 ∧ 𝐴 ∈ 𝑅 ) → ∃ 𝑥 ∃ 𝑦 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ )

Proof

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