# Metamath Proof Explorer

## Theorem opabdm

Description: Domain of an ordered-pair class abstraction. (Contributed by Thierry Arnoux, 31-Aug-2017)

Ref Expression
Assertion opabdm ${⊢}{R}=\left\{⟨{x},{y}⟩|{\phi }\right\}\to \mathrm{dom}{R}=\left\{{x}|\exists {y}\phantom{\rule{.4em}{0ex}}{\phi }\right\}$

### Proof

Step Hyp Ref Expression
1 df-dm ${⊢}\mathrm{dom}{R}=\left\{{x}|\exists {y}\phantom{\rule{.4em}{0ex}}{x}{R}{y}\right\}$
2 nfopab1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left\{⟨{x},{y}⟩|{\phi }\right\}$
3 2 nfeq2 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{R}=\left\{⟨{x},{y}⟩|{\phi }\right\}$
4 nfopab2 ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}\left\{⟨{x},{y}⟩|{\phi }\right\}$
5 4 nfeq2 ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{R}=\left\{⟨{x},{y}⟩|{\phi }\right\}$
6 df-br ${⊢}{x}{R}{y}↔⟨{x},{y}⟩\in {R}$
7 eleq2 ${⊢}{R}=\left\{⟨{x},{y}⟩|{\phi }\right\}\to \left(⟨{x},{y}⟩\in {R}↔⟨{x},{y}⟩\in \left\{⟨{x},{y}⟩|{\phi }\right\}\right)$
8 opabidw ${⊢}⟨{x},{y}⟩\in \left\{⟨{x},{y}⟩|{\phi }\right\}↔{\phi }$
9 7 8 syl6bb ${⊢}{R}=\left\{⟨{x},{y}⟩|{\phi }\right\}\to \left(⟨{x},{y}⟩\in {R}↔{\phi }\right)$
10 6 9 syl5bb ${⊢}{R}=\left\{⟨{x},{y}⟩|{\phi }\right\}\to \left({x}{R}{y}↔{\phi }\right)$
11 5 10 exbid ${⊢}{R}=\left\{⟨{x},{y}⟩|{\phi }\right\}\to \left(\exists {y}\phantom{\rule{.4em}{0ex}}{x}{R}{y}↔\exists {y}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
12 3 11 abbid ${⊢}{R}=\left\{⟨{x},{y}⟩|{\phi }\right\}\to \left\{{x}|\exists {y}\phantom{\rule{.4em}{0ex}}{x}{R}{y}\right\}=\left\{{x}|\exists {y}\phantom{\rule{.4em}{0ex}}{\phi }\right\}$
13 1 12 syl5eq ${⊢}{R}=\left\{⟨{x},{y}⟩|{\phi }\right\}\to \mathrm{dom}{R}=\left\{{x}|\exists {y}\phantom{\rule{.4em}{0ex}}{\phi }\right\}$