# Metamath Proof Explorer

## Theorem nulmo

Description: There exists at most one empty set. With either axnul or axnulALT or ax-nul , this proves that there exists a unique empty set. In practice, once the language of classes is available, we use the stronger characterization among classes eq0 . (Contributed by NM, 22-Dec-2007) Use the at-most-one quantifier. (Revised by BJ, 17-Sep-2022) (Proof shortened by Wolf Lammen, 26-Apr-2023)

Ref Expression
Assertion nulmo ${⊢}{\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}¬{y}\in {x}$

### Proof

Step Hyp Ref Expression
1 nfv ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\perp$
2 1 axextmo ${⊢}{\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {x}↔\perp \right)$
3 nbfal ${⊢}¬{y}\in {x}↔\left({y}\in {x}↔\perp \right)$
4 3 albii ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}¬{y}\in {x}↔\forall {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {x}↔\perp \right)$
5 4 mobii ${⊢}{\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}¬{y}\in {x}↔{\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {x}↔\perp \right)$
6 2 5 mpbir ${⊢}{\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}¬{y}\in {x}$