# Metamath Proof Explorer

## Theorem dm0rn0

Description: An empty domain is equivalent to an empty range. (Contributed by NM, 21-May-1998)

Ref Expression
Assertion dm0rn0 ${⊢}\mathrm{dom}{A}=\varnothing ↔\mathrm{ran}{A}=\varnothing$

### Proof

Step Hyp Ref Expression
1 alnex ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}¬\exists {y}\phantom{\rule{.4em}{0ex}}{x}{A}{y}↔¬\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}{x}{A}{y}$
2 excom ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}{x}{A}{y}↔\exists {y}\phantom{\rule{.4em}{0ex}}\exists {x}\phantom{\rule{.4em}{0ex}}{x}{A}{y}$
3 1 2 xchbinx ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}¬\exists {y}\phantom{\rule{.4em}{0ex}}{x}{A}{y}↔¬\exists {y}\phantom{\rule{.4em}{0ex}}\exists {x}\phantom{\rule{.4em}{0ex}}{x}{A}{y}$
4 alnex ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}¬\exists {x}\phantom{\rule{.4em}{0ex}}{x}{A}{y}↔¬\exists {y}\phantom{\rule{.4em}{0ex}}\exists {x}\phantom{\rule{.4em}{0ex}}{x}{A}{y}$
5 3 4 bitr4i ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}¬\exists {y}\phantom{\rule{.4em}{0ex}}{x}{A}{y}↔\forall {y}\phantom{\rule{.4em}{0ex}}¬\exists {x}\phantom{\rule{.4em}{0ex}}{x}{A}{y}$
6 noel ${⊢}¬{x}\in \varnothing$
7 6 nbn ${⊢}¬\exists {y}\phantom{\rule{.4em}{0ex}}{x}{A}{y}↔\left(\exists {y}\phantom{\rule{.4em}{0ex}}{x}{A}{y}↔{x}\in \varnothing \right)$
8 7 albii ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}¬\exists {y}\phantom{\rule{.4em}{0ex}}{x}{A}{y}↔\forall {x}\phantom{\rule{.4em}{0ex}}\left(\exists {y}\phantom{\rule{.4em}{0ex}}{x}{A}{y}↔{x}\in \varnothing \right)$
9 noel ${⊢}¬{y}\in \varnothing$
10 9 nbn ${⊢}¬\exists {x}\phantom{\rule{.4em}{0ex}}{x}{A}{y}↔\left(\exists {x}\phantom{\rule{.4em}{0ex}}{x}{A}{y}↔{y}\in \varnothing \right)$
11 10 albii ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}¬\exists {x}\phantom{\rule{.4em}{0ex}}{x}{A}{y}↔\forall {y}\phantom{\rule{.4em}{0ex}}\left(\exists {x}\phantom{\rule{.4em}{0ex}}{x}{A}{y}↔{y}\in \varnothing \right)$
12 5 8 11 3bitr3i ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left(\exists {y}\phantom{\rule{.4em}{0ex}}{x}{A}{y}↔{x}\in \varnothing \right)↔\forall {y}\phantom{\rule{.4em}{0ex}}\left(\exists {x}\phantom{\rule{.4em}{0ex}}{x}{A}{y}↔{y}\in \varnothing \right)$
13 abeq1 ${⊢}\left\{{x}|\exists {y}\phantom{\rule{.4em}{0ex}}{x}{A}{y}\right\}=\varnothing ↔\forall {x}\phantom{\rule{.4em}{0ex}}\left(\exists {y}\phantom{\rule{.4em}{0ex}}{x}{A}{y}↔{x}\in \varnothing \right)$
14 abeq1 ${⊢}\left\{{y}|\exists {x}\phantom{\rule{.4em}{0ex}}{x}{A}{y}\right\}=\varnothing ↔\forall {y}\phantom{\rule{.4em}{0ex}}\left(\exists {x}\phantom{\rule{.4em}{0ex}}{x}{A}{y}↔{y}\in \varnothing \right)$
15 12 13 14 3bitr4i ${⊢}\left\{{x}|\exists {y}\phantom{\rule{.4em}{0ex}}{x}{A}{y}\right\}=\varnothing ↔\left\{{y}|\exists {x}\phantom{\rule{.4em}{0ex}}{x}{A}{y}\right\}=\varnothing$
16 df-dm ${⊢}\mathrm{dom}{A}=\left\{{x}|\exists {y}\phantom{\rule{.4em}{0ex}}{x}{A}{y}\right\}$
17 16 eqeq1i ${⊢}\mathrm{dom}{A}=\varnothing ↔\left\{{x}|\exists {y}\phantom{\rule{.4em}{0ex}}{x}{A}{y}\right\}=\varnothing$
18 dfrn2 ${⊢}\mathrm{ran}{A}=\left\{{y}|\exists {x}\phantom{\rule{.4em}{0ex}}{x}{A}{y}\right\}$
19 18 eqeq1i ${⊢}\mathrm{ran}{A}=\varnothing ↔\left\{{y}|\exists {x}\phantom{\rule{.4em}{0ex}}{x}{A}{y}\right\}=\varnothing$
20 15 17 19 3bitr4i ${⊢}\mathrm{dom}{A}=\varnothing ↔\mathrm{ran}{A}=\varnothing$