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 𝑅 ∧ 𝐴 ∈ 𝑅 ) → ( 1st ‘ 𝐴 ) ∈ dom 𝑅 )

Proof

Step	Hyp	Ref	Expression
1		df-rel	⊢ ( Rel 𝑅 ↔ 𝑅 ⊆ ( V × V ) )
2	1	biimpi	⊢ ( Rel 𝑅 → 𝑅 ⊆ ( V × V ) )
3	2	sselda	⊢ ( ( Rel 𝑅 ∧ 𝐴 ∈ 𝑅 ) → 𝐴 ∈ ( V × V ) )
4		1stval2	⊢ ( 𝐴 ∈ ( V × V ) → ( 1st ‘ 𝐴 ) = ∩ ∩ 𝐴 )
5	3 4	syl	⊢ ( ( Rel 𝑅 ∧ 𝐴 ∈ 𝑅 ) → ( 1st ‘ 𝐴 ) = ∩ ∩ 𝐴 )
6		elreldm	⊢ ( ( Rel 𝑅 ∧ 𝐴 ∈ 𝑅 ) → ∩ ∩ 𝐴 ∈ dom 𝑅 )
7	5 6	eqeltrd	⊢ ( ( Rel 𝑅 ∧ 𝐴 ∈ 𝑅 ) → ( 1st ‘ 𝐴 ) ∈ dom 𝑅 )