Theorem iotan0aiotaex

Description: If the iota over a wff ph is not empty, the alternate iota over ph is a set. (Contributed by AV, 25-Aug-2022)

	Ref	Expression
Assertion	iotan0aiotaex	$$⊢\left(\iota x|\phi \right)\ne \varnothing \to \iota \in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		iotanul	$$⊢\neg \exists !x\phi \to \left(\iota x|\phi \right)=\varnothing$$
2	1	necon1ai	$$⊢\left(\iota x|\phi \right)\ne \varnothing \to \exists !x\phi$$
3		aiotaexb	$$⊢\exists !x\phi \leftrightarrow \iota \in \mathrm{V}$$
4	2 3	sylib	$$⊢\left(\iota x|\phi \right)\ne \varnothing \to \iota \in \mathrm{V}$$