Theorem bj-nuliota

Description: Definition of the empty set using the definite description binder. See also bj-nuliotaALT . (Contributed by BJ, 30-Nov-2019) (Proof modification is discouraged.)

	Ref	Expression
Assertion	bj-nuliota	$$⊢\varnothing =\left(\iota x|\forall y\neg y\in x\right)$$

Proof

Step	Hyp	Ref	Expression
1		0ex	$$⊢\varnothing \in \mathrm{V}$$
2	1	eueqi	$$⊢\exists !xx=\varnothing$$
3		eq0	$$⊢x=\varnothing \leftrightarrow \forall y\neg y\in x$$
4	3	eubii	$$⊢\exists !xx=\varnothing \leftrightarrow \exists !x\forall y\neg y\in x$$
5	2 4	mpbi	$$⊢\exists !x\forall y\neg y\in x$$
6		eleq2	$$⊢x=\varnothing \to \left(y\in x\leftrightarrow y\in \varnothing \right)$$
7	6	notbid	$$⊢x=\varnothing \to \left(\neg y\in x\leftrightarrow \neg y\in \varnothing \right)$$
8	7	albidv	$$⊢x=\varnothing \to \left(\forall y\neg y\in x\leftrightarrow \forall y\neg y\in \varnothing \right)$$
9	8	iota2	$$⊢\left(\varnothing \in \mathrm{V}\wedge \exists !x\forall y\neg y\in x\right)\to \left(\forall y\neg y\in \varnothing \leftrightarrow \left(\iota x|\forall y\neg y\in x\right)=\varnothing \right)$$
10	1 5 9	mp2an	$$⊢\forall y\neg y\in \varnothing \leftrightarrow \left(\iota x|\forall y\neg y\in x\right)=\varnothing$$
11		noel	$$⊢\neg y\in \varnothing$$
12	10 11	mpgbi	$$⊢\left(\iota x|\forall y\neg y\in x\right)=\varnothing$$
13	12	eqcomi	$$⊢\varnothing =\left(\iota x|\forall y\neg y\in x\right)$$