Theorem eu0

Description: There is only one empty set. (Contributed by RP, 1-Oct-2023)

	Ref	Expression
Assertion	eu0	$$⊢\left(\forall x\neg x\in \varnothing \wedge \exists !x\forall y\neg y\in x\right)$$

Proof

Step	Hyp	Ref	Expression
1		noel	$$⊢\neg x\in \varnothing$$
2	1	ax-gen	$$⊢\forall x\neg x\in \varnothing$$
3		ax-nul	$$⊢\exists x\forall y\neg y\in x$$
4		nulmo	$$⊢{\exists }^{*}x\forall y\neg y\in x$$
5		df-eu	$$⊢\exists !x\forall y\neg y\in x\leftrightarrow \left(\exists x\forall y\neg y\in x\wedge {\exists }^{*}x\forall y\neg y\in x\right)$$
6	3 4 5	mpbir2an	$$⊢\exists !x\forall y\neg y\in x$$
7	2 6	pm3.2i	$$⊢\left(\forall x\neg x\in \varnothing \wedge \exists !x\forall y\neg y\in x\right)$$