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\forall y\neg y\in x$$

Proof

Step	Hyp	Ref	Expression
1		nfv	$$⊢Ⅎx\perp$$
2	1	axextmo	$$⊢{\exists }^{*}x\forall y\left(y\in x\leftrightarrow \perp \right)$$
3		nbfal	$$⊢\neg y\in x\leftrightarrow \left(y\in x\leftrightarrow \perp \right)$$
4	3	albii	$$⊢\forall y\neg y\in x\leftrightarrow \forall y\left(y\in x\leftrightarrow \perp \right)$$
5	4	mobii	$$⊢{\exists }^{*}x\forall y\neg y\in x\leftrightarrow {\exists }^{*}x\forall y\left(y\in x\leftrightarrow \perp \right)$$
6	2 5	mpbir	$$⊢{\exists }^{*}x\forall y\neg y\in x$$