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) Remove dependency on ax-10 , ax-11 , ax-12 . (Revised by SN, 6-Nov-2024)

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

Proof

Step	Hyp	Ref	Expression
1		iotaval2	$$⊢\left\{x|\phi \right\}=\left\{y\right\}\to \left(\iota x|\phi \right)=y$$
2		vex	$$⊢y\in \mathrm{V}$$
3	1 2	eqeltrdi	$$⊢\left\{x|\phi \right\}=\left\{y\right\}\to \left(\iota x|\phi \right)\in \mathrm{V}$$
4	3	exlimiv	$$⊢\exists y\left\{x|\phi \right\}=\left\{y\right\}\to \left(\iota x|\phi \right)\in \mathrm{V}$$
5		iotanul2	$$⊢\neg \exists y\left\{x|\phi \right\}=\left\{y\right\}\to \left(\iota x|\phi \right)=\varnothing$$
6		0ex	$$⊢\varnothing \in \mathrm{V}$$
7	5 6	eqeltrdi	$$⊢\neg \exists y\left\{x|\phi \right\}=\left\{y\right\}\to \left(\iota x|\phi \right)\in \mathrm{V}$$
8	4 7	pm2.61i	$$⊢\left(\iota x|\phi \right)\in \mathrm{V}$$