Theorem iotaex

Description: Theorem 8.23 in Quine p. 58. This theorem proves the existence of the iota class under our definition. (Contributed by Andrew Salmon, 11-Jul-2011)

	Ref	Expression
Assertion	iotaex	$$⊢\left(\iota x|\phi \right)\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		iotaval	$$⊢\forall x\left(\phi \leftrightarrow x=z\right)\to \left(\iota x|\phi \right)=z$$
2	1	eqcomd	$$⊢\forall x\left(\phi \leftrightarrow x=z\right)\to z=\left(\iota x|\phi \right)$$
3	2	eximi	$$⊢\exists z\forall x\left(\phi \leftrightarrow x=z\right)\to \exists zz=\left(\iota x|\phi \right)$$
4		eu6	$$⊢\exists !x\phi \leftrightarrow \exists z\forall x\left(\phi \leftrightarrow x=z\right)$$
5		isset	$$⊢\left(\iota x|\phi \right)\in \mathrm{V}\leftrightarrow \exists zz=\left(\iota x|\phi \right)$$
6	3 4 5	3imtr4i	$$⊢\exists !x\phi \to \left(\iota x|\phi \right)\in \mathrm{V}$$
7		iotanul	$$⊢\neg \exists !x\phi \to \left(\iota x|\phi \right)=\varnothing$$
8		0ex	$$⊢\varnothing \in \mathrm{V}$$
9	7 8	eqeltrdi	$$⊢\neg \exists !x\phi \to \left(\iota x|\phi \right)\in \mathrm{V}$$
10	6 9	pm2.61i	$$⊢\left(\iota x|\phi \right)\in \mathrm{V}$$