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	$$⊢\phi \to A\in V$$
	opeldmd.2	$$⊢\phi \to B\in W$$
Assertion	opeldmd	$$⊢\phi \to \left(⟨A,B⟩\in C\to A\in \mathrm{dom}C\right)$$

Proof

Step	Hyp	Ref	Expression
1		opeldmd.1	$$⊢\phi \to A\in V$$
2		opeldmd.2	$$⊢\phi \to B\in W$$
3		opeq2	$$⊢y=B\to ⟨A,y⟩=⟨A,B⟩$$
4	3	eleq1d	$$⊢y=B\to \left(⟨A,y⟩\in C\leftrightarrow ⟨A,B⟩\in C\right)$$
5	4	spcegv	$$⊢B\in W\to \left(⟨A,B⟩\in C\to \exists y⟨A,y⟩\in C\right)$$
6	2 5	syl	$$⊢\phi \to \left(⟨A,B⟩\in C\to \exists y⟨A,y⟩\in C\right)$$
7		eldm2g	$$⊢A\in V\to \left(A\in \mathrm{dom}C\leftrightarrow \exists y⟨A,y⟩\in C\right)$$
8	1 7	syl	$$⊢\phi \to \left(A\in \mathrm{dom}C\leftrightarrow \exists y⟨A,y⟩\in C\right)$$
9	6 8	sylibrd	$$⊢\phi \to \left(⟨A,B⟩\in C\to A\in \mathrm{dom}C\right)$$