Theorem iota0ndef

Description: Example for an undefined iota being the empty 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). (Contributed by AV, 24-Aug-2022)

	Ref	Expression
Assertion	iota0ndef	$$⊢\left(\iota x|\forall yy\in x\right)=\varnothing$$

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		iotanul	$$⊢\neg \exists !x\forall yy\in x\to \left(\iota x|\forall yy\in x\right)=\varnothing$$
6	4 5	ax-mp	$$⊢\left(\iota x|\forall yy\in x\right)=\varnothing$$