Theorem aiota0ndef

Description: Example for an undefined alternate iota being no set, i.e., A. y y e. x is a wff not satisfied by a (unique) value x (there is no set, and therefore certainly no unique set, which contains every set). This is different from iota0ndef , where the iota still is a set (the empty set). (Contributed by AV, 25-Aug-2022)

	Ref	Expression
Assertion	aiota0ndef	$$⊢\iota \notin \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		nalset	$$⊢\neg \exists x\forall yy\in x$$
2	1	intnanr	$$⊢\neg \left(\exists x\forall yy\in x\wedge {\exists }^{*}x\forall yy\in x\right)$$
3		df-eu	$$⊢\exists !x\forall yy\in x\leftrightarrow \left(\exists x\forall yy\in x\wedge {\exists }^{*}x\forall yy\in x\right)$$
4	2 3	mtbir	$$⊢\neg \exists !x\forall yy\in x$$
5		df-nel	$$⊢\iota \notin \mathrm{V}\leftrightarrow \neg \iota \in \mathrm{V}$$
6		aiotaexb	$$⊢\exists !x\forall yy\in x\leftrightarrow \iota \in \mathrm{V}$$
7	5 6	xchbinxr	$$⊢\iota \notin \mathrm{V}\leftrightarrow \neg \exists !x\forall yy\in x$$
8	4 7	mpbir	$$⊢\iota \notin \mathrm{V}$$