Theorem aiotavb

Description: The alternate iota over a wff ph is the universe iff there is no unique value x satisfying ph . (Contributed by AV, 25-Aug-2022)

	Ref	Expression
Assertion	aiotavb	$$⊢\neg \exists !x\phi \leftrightarrow \iota =\mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		intnex	$$⊢\neg \bigcap \left\{y|\left\{x|\phi \right\}=\left\{y\right\}\right\}\in \mathrm{V}\leftrightarrow \bigcap \left\{y|\left\{x|\phi \right\}=\left\{y\right\}\right\}=\mathrm{V}$$
2		df-aiota	$$⊢\iota =\bigcap \left\{y|\left\{x|\phi \right\}=\left\{y\right\}\right\}$$
3	2	eleq1i	$$⊢\iota \in \mathrm{V}\leftrightarrow \bigcap \left\{y|\left\{x|\phi \right\}=\left\{y\right\}\right\}\in \mathrm{V}$$
4	3	notbii	$$⊢\neg \iota \in \mathrm{V}\leftrightarrow \neg \bigcap \left\{y|\left\{x|\phi \right\}=\left\{y\right\}\right\}\in \mathrm{V}$$
5	2	eqeq1i	$$⊢\iota =\mathrm{V}\leftrightarrow \bigcap \left\{y|\left\{x|\phi \right\}=\left\{y\right\}\right\}=\mathrm{V}$$
6	1 4 5	3bitr4i	$$⊢\neg \iota \in \mathrm{V}\leftrightarrow \iota =\mathrm{V}$$
7		aiotaexb	$$⊢\exists !x\phi \leftrightarrow \iota \in \mathrm{V}$$
8	6 7	xchnxbir	$$⊢\neg \exists !x\phi \leftrightarrow \iota =\mathrm{V}$$