Theorem aiotaexb

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

	Ref	Expression
Assertion	aiotaexb	$$⊢\exists !x\phi \leftrightarrow \iota \in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		intexab	$$⊢\exists y\left\{x|\phi \right\}=\left\{y\right\}\leftrightarrow \bigcap \left\{y|\left\{x|\phi \right\}=\left\{y\right\}\right\}\in \mathrm{V}$$
2		euabsn2	$$⊢\exists !x\phi \leftrightarrow \exists y\left\{x|\phi \right\}=\left\{y\right\}$$
3		df-aiota	$$⊢\iota =\bigcap \left\{y|\left\{x|\phi \right\}=\left\{y\right\}\right\}$$
4	3	eleq1i	$$⊢\iota \in \mathrm{V}\leftrightarrow \bigcap \left\{y|\left\{x|\phi \right\}=\left\{y\right\}\right\}\in \mathrm{V}$$
5	1 2 4	3bitr4i	$$⊢\exists !x\phi \leftrightarrow \iota \in \mathrm{V}$$