# Metamath Proof Explorer

## 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}\phantom{\rule{.4em}{0ex}}⟨{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}⟩↔⟨{x},{B}⟩=⟨{A},{B}⟩\right)$
8 7 spcegv ${⊢}{B}\in {V}\to \left(⟨{x},{B}⟩=⟨{A},{B}⟩\to \exists {y}\phantom{\rule{.4em}{0ex}}⟨{x},{y}⟩=⟨{A},{B}⟩\right)$
9 5 8 syl5 ${⊢}{B}\in {V}\to \left({x}={A}\to \exists {y}\phantom{\rule{.4em}{0ex}}⟨{x},{y}⟩=⟨{A},{B}⟩\right)$
10 4 9 impbid2 ${⊢}{B}\in {V}\to \left(\exists {y}\phantom{\rule{.4em}{0ex}}⟨{x},{y}⟩=⟨{A},{B}⟩↔{x}={A}\right)$
11 1 eldm2 ${⊢}{x}\in \mathrm{dom}\left\{⟨{A},{B}⟩\right\}↔\exists {y}\phantom{\rule{.4em}{0ex}}⟨{x},{y}⟩\in \left\{⟨{A},{B}⟩\right\}$
12 opex ${⊢}⟨{x},{y}⟩\in \mathrm{V}$
13 12 elsn ${⊢}⟨{x},{y}⟩\in \left\{⟨{A},{B}⟩\right\}↔⟨{x},{y}⟩=⟨{A},{B}⟩$
14 13 exbii ${⊢}\exists {y}\phantom{\rule{.4em}{0ex}}⟨{x},{y}⟩\in \left\{⟨{A},{B}⟩\right\}↔\exists {y}\phantom{\rule{.4em}{0ex}}⟨{x},{y}⟩=⟨{A},{B}⟩$
15 11 14 bitri ${⊢}{x}\in \mathrm{dom}\left\{⟨{A},{B}⟩\right\}↔\exists {y}\phantom{\rule{.4em}{0ex}}⟨{x},{y}⟩=⟨{A},{B}⟩$
16 velsn ${⊢}{x}\in \left\{{A}\right\}↔{x}={A}$
17 10 15 16 3bitr4g ${⊢}{B}\in {V}\to \left({x}\in \mathrm{dom}\left\{⟨{A},{B}⟩\right\}↔{x}\in \left\{{A}\right\}\right)$
18 17 eqrdv ${⊢}{B}\in {V}\to \mathrm{dom}\left\{⟨{A},{B}⟩\right\}=\left\{{A}\right\}$