This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem elrel

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

		Ref	Expression
	Assertion	elrel	$⊢ (Rel R \land A \in R) \to \exists x \exists y A = ⟨x, y⟩$

Step	Hyp	Ref	Expression
1		df-rel	$⊢ Rel R \leftrightarrow R \subseteq V \times V$
2	1	biimpi	$⊢ Rel R \to R \subseteq V \times V$
3	2	sselda	$⊢ (Rel R \land A \in R) \to A \in (V \times V)$
4		elvv	$⊢ A \in (V \times V) \leftrightarrow \exists x \exists y A = ⟨x, y⟩$
5	3 4	sylib	$⊢ (Rel R \land A \in R) \to \exists x \exists y A = ⟨x, y⟩$