# Metamath Proof Explorer

## Theorem reldm0

Description: A relation is empty iff its domain is empty. (Contributed by NM, 15-Sep-2004)

Ref Expression
Assertion reldm0 ${⊢}\mathrm{Rel}{A}\to \left({A}=\varnothing ↔\mathrm{dom}{A}=\varnothing \right)$

### Proof

Step Hyp Ref Expression
1 rel0 ${⊢}\mathrm{Rel}\varnothing$
2 eqrel ${⊢}\left(\mathrm{Rel}{A}\wedge \mathrm{Rel}\varnothing \right)\to \left({A}=\varnothing ↔\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(⟨{x},{y}⟩\in {A}↔⟨{x},{y}⟩\in \varnothing \right)\right)$
3 1 2 mpan2 ${⊢}\mathrm{Rel}{A}\to \left({A}=\varnothing ↔\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(⟨{x},{y}⟩\in {A}↔⟨{x},{y}⟩\in \varnothing \right)\right)$
4 eq0 ${⊢}\mathrm{dom}{A}=\varnothing ↔\forall {x}\phantom{\rule{.4em}{0ex}}¬{x}\in \mathrm{dom}{A}$
5 alnex ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}¬⟨{x},{y}⟩\in {A}↔¬\exists {y}\phantom{\rule{.4em}{0ex}}⟨{x},{y}⟩\in {A}$
6 vex ${⊢}{x}\in \mathrm{V}$
7 6 eldm2 ${⊢}{x}\in \mathrm{dom}{A}↔\exists {y}\phantom{\rule{.4em}{0ex}}⟨{x},{y}⟩\in {A}$
8 5 7 xchbinxr ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}¬⟨{x},{y}⟩\in {A}↔¬{x}\in \mathrm{dom}{A}$
9 noel ${⊢}¬⟨{x},{y}⟩\in \varnothing$
10 9 nbn ${⊢}¬⟨{x},{y}⟩\in {A}↔\left(⟨{x},{y}⟩\in {A}↔⟨{x},{y}⟩\in \varnothing \right)$
11 10 albii ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}¬⟨{x},{y}⟩\in {A}↔\forall {y}\phantom{\rule{.4em}{0ex}}\left(⟨{x},{y}⟩\in {A}↔⟨{x},{y}⟩\in \varnothing \right)$
12 8 11 bitr3i ${⊢}¬{x}\in \mathrm{dom}{A}↔\forall {y}\phantom{\rule{.4em}{0ex}}\left(⟨{x},{y}⟩\in {A}↔⟨{x},{y}⟩\in \varnothing \right)$
13 12 albii ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}¬{x}\in \mathrm{dom}{A}↔\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(⟨{x},{y}⟩\in {A}↔⟨{x},{y}⟩\in \varnothing \right)$
14 4 13 bitr2i ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(⟨{x},{y}⟩\in {A}↔⟨{x},{y}⟩\in \varnothing \right)↔\mathrm{dom}{A}=\varnothing$
15 3 14 syl6bb ${⊢}\mathrm{Rel}{A}\to \left({A}=\varnothing ↔\mathrm{dom}{A}=\varnothing \right)$