Theorem opeldm

Description: Membership of first of an ordered pair in a domain. (Contributed by NM, 30-Jul-1995)

	Ref	Expression
Hypotheses	opeldm.1	⊢ 𝐴 ∈ V
	opeldm.2	⊢ 𝐵 ∈ V
Assertion	opeldm	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝐶 → 𝐴 ∈ dom 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		opeldm.1	⊢ 𝐴 ∈ V
2		opeldm.2	⊢ 𝐵 ∈ V
3		opeq2	⊢ ( 𝑦 = 𝐵 → ⟨ 𝐴 , 𝑦 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ )
4	3	eleq1d	⊢ ( 𝑦 = 𝐵 → ( ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐶 ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝐶 ) )
5	2 4	spcev	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝐶 → ∃ 𝑦 ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐶 )
6	1	eldm2	⊢ ( 𝐴 ∈ dom 𝐶 ↔ ∃ 𝑦 ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐶 )
7	5 6	sylibr	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝐶 → 𝐴 ∈ dom 𝐶 )