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

Metamath Proof Explorer

Theorem 1stdm

Description: The first ordered pair component of a member of a relation belongs to the domain of the relation. (Contributed by NM, 17-Sep-2006)

		Ref	Expression
	Assertion	1stdm	$⊢ (Rel R \land A \in R) \to 1^{st} (A) \in dom R$

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		1stval2	$⊢ A \in (V \times V) \to 1^{st} (A) = ⋂ ⋂ A$
5	3 4	syl	$⊢ (Rel R \land A \in R) \to 1^{st} (A) = ⋂ ⋂ A$
6		elreldm	$⊢ (Rel R \land A \in R) \to ⋂ ⋂ A \in dom R$
7	5 6	eqeltrd	$⊢ (Rel R \land A \in R) \to 1^{st} (A) \in dom R$