Theorem opeldmd

Description: Membership of first of an ordered pair in a domain. Deduction version of opeldm . (Contributed by AV, 11-Mar-2021)

	Ref	Expression
Hypotheses	opeldmd.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	opeldmd.2	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
Assertion	opeldmd	⊢ ( 𝜑 → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝐶 → 𝐴 ∈ dom 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		opeldmd.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2		opeldmd.2	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
3		opeq2	⊢ ( 𝑦 = 𝐵 → ⟨ 𝐴 , 𝑦 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ )
4	3	eleq1d	⊢ ( 𝑦 = 𝐵 → ( ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐶 ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝐶 ) )
5	4	spcegv	⊢ ( 𝐵 ∈ 𝑊 → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝐶 → ∃ 𝑦 ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐶 ) )
6	2 5	syl	⊢ ( 𝜑 → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝐶 → ∃ 𝑦 ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐶 ) )
7		eldm2g	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ dom 𝐶 ↔ ∃ 𝑦 ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐶 ) )
8	1 7	syl	⊢ ( 𝜑 → ( 𝐴 ∈ dom 𝐶 ↔ ∃ 𝑦 ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐶 ) )
9	6 8	sylibrd	⊢ ( 𝜑 → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝐶 → 𝐴 ∈ dom 𝐶 ) )