Theorem sn-iotaex

Description: iotaex without ax-10 , ax-11 , ax-12 . (Contributed by SN, 6-Nov-2024)

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

Proof

Step	Hyp	Ref	Expression
1		sn-iotaval	$$⊢\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		sn-iotanul	$$⊢\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}$$