Theorem opeldm

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

	Ref	Expression
Hypotheses	opeldm.1	$$⊢A\in \mathrm{V}$$
	opeldm.2	$$⊢B\in \mathrm{V}$$
Assertion	opeldm	$$⊢⟨A,B⟩\in C\to A\in \mathrm{dom}C$$

Proof

Step	Hyp	Ref	Expression
1		opeldm.1	$$⊢A\in \mathrm{V}$$
2		opeldm.2	$$⊢B\in \mathrm{V}$$
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	2 4	spcev	$$⊢⟨A,B⟩\in C\to \exists y⟨A,y⟩\in C$$
6	1	eldm2	$$⊢A\in \mathrm{dom}C\leftrightarrow \exists y⟨A,y⟩\in C$$
7	5 6	sylibr	$$⊢⟨A,B⟩\in C\to A\in \mathrm{dom}C$$