Theorem iotaexeu

Description: The iota class exists. This theorem does not require ax-nul for its proof. (Contributed by Andrew Salmon, 11-Jul-2011)

	Ref	Expression
Assertion	iotaexeu	$$⊢\exists !x\phi \to \left(\iota x|\phi \right)\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		iotaval	$$⊢\forall x\left(\phi \leftrightarrow x=y\right)\to \left(\iota x|\phi \right)=y$$
2	1	eqcomd	$$⊢\forall x\left(\phi \leftrightarrow x=y\right)\to y=\left(\iota x|\phi \right)$$
3	2	eximi	$$⊢\exists y\forall x\left(\phi \leftrightarrow x=y\right)\to \exists yy=\left(\iota x|\phi \right)$$
4		eu6	$$⊢\exists !x\phi \leftrightarrow \exists y\forall x\left(\phi \leftrightarrow x=y\right)$$
5		isset	$$⊢\left(\iota x|\phi \right)\in \mathrm{V}\leftrightarrow \exists yy=\left(\iota x|\phi \right)$$
6	3 4 5	3imtr4i	$$⊢\exists !x\phi \to \left(\iota x|\phi \right)\in \mathrm{V}$$