Theorem dmsnopg

Description: The domain of a singleton of an ordered pair is the singleton of the first member. (Contributed by Mario Carneiro, 26-Apr-2015)

	Ref	Expression
Assertion	dmsnopg	$$⊢B\in V\to \mathrm{dom}\left\{⟨A,B⟩\right\}=\left\{A\right\}$$

Proof

Step	Hyp	Ref	Expression
1		vex	$$⊢x\in \mathrm{V}$$
2		vex	$$⊢y\in \mathrm{V}$$
3	1 2	opth1	$$⊢⟨x,y⟩=⟨A,B⟩\to x=A$$
4	3	exlimiv	$$⊢\exists y⟨x,y⟩=⟨A,B⟩\to x=A$$
5		opeq1	$$⊢x=A\to ⟨x,B⟩=⟨A,B⟩$$
6		opeq2	$$⊢y=B\to ⟨x,y⟩=⟨x,B⟩$$
7	6	eqeq1d	$$⊢y=B\to \left(⟨x,y⟩=⟨A,B⟩\leftrightarrow ⟨x,B⟩=⟨A,B⟩\right)$$
8	7	spcegv	$$⊢B\in V\to \left(⟨x,B⟩=⟨A,B⟩\to \exists y⟨x,y⟩=⟨A,B⟩\right)$$
9	5 8	syl5	$$⊢B\in V\to \left(x=A\to \exists y⟨x,y⟩=⟨A,B⟩\right)$$
10	4 9	impbid2	$$⊢B\in V\to \left(\exists y⟨x,y⟩=⟨A,B⟩\leftrightarrow x=A\right)$$
11	1	eldm2	$$⊢x\in \mathrm{dom}\left\{⟨A,B⟩\right\}\leftrightarrow \exists y⟨x,y⟩\in \left\{⟨A,B⟩\right\}$$
12		opex	$$⊢⟨x,y⟩\in \mathrm{V}$$
13	12	elsn	$$⊢⟨x,y⟩\in \left\{⟨A,B⟩\right\}\leftrightarrow ⟨x,y⟩=⟨A,B⟩$$
14	13	exbii	$$⊢\exists y⟨x,y⟩\in \left\{⟨A,B⟩\right\}\leftrightarrow \exists y⟨x,y⟩=⟨A,B⟩$$
15	11 14	bitri	$$⊢x\in \mathrm{dom}\left\{⟨A,B⟩\right\}\leftrightarrow \exists y⟨x,y⟩=⟨A,B⟩$$
16		velsn	$$⊢x\in \left\{A\right\}\leftrightarrow x=A$$
17	10 15 16	3bitr4g	$$⊢B\in V\to \left(x\in \mathrm{dom}\left\{⟨A,B⟩\right\}\leftrightarrow x\in \left\{A\right\}\right)$$
18	17	eqrdv	$$⊢B\in V\to \mathrm{dom}\left\{⟨A,B⟩\right\}=\left\{A\right\}$$