Theorem aiotaexim

Description: Representation of "the unique element such that ph " with a class expression A which is a set (that means that "the unique element such that ph " exists). Analog to iotan0 which requires A to be nonempty instead of being a set. That gives a more natural statement, closer to statements like spcgv . (Proposed by BJ, 18-Oct-2026.) (Contributed by AV, 18-Oct-2026)

	Ref	Expression
Hypothesis	aiotaexim.1	$$⊢x=A\to \left(\phi \leftrightarrow \psi \right)$$
Assertion	aiotaexim	$$⊢\left(A\in V\wedge A=\iota \right)\to \psi$$

Proof

Step	Hyp	Ref	Expression
1		aiotaexim.1	$$⊢x=A\to \left(\phi \leftrightarrow \psi \right)$$
2		dfaiota3	$$⊢\iota =if\left(\exists !x\phi ,\bigcap \left\{x|\phi \right\},\mathrm{V}\right)$$
3	2	eqeq2i	$$⊢A=\iota \leftrightarrow A=if\left(\exists !x\phi ,\bigcap \left\{x|\phi \right\},\mathrm{V}\right)$$
4		iftrue	$$⊢\exists !x\phi \to if\left(\exists !x\phi ,\bigcap \left\{x|\phi \right\},\mathrm{V}\right)=\bigcap \left\{x|\phi \right\}$$
5	4	eqeq2d	$$⊢\exists !x\phi \to \left(A=if\left(\exists !x\phi ,\bigcap \left\{x|\phi \right\},\mathrm{V}\right)\leftrightarrow A=\bigcap \left\{x|\phi \right\}\right)$$
6		iotain	$$⊢\exists !x\phi \to \bigcap \left\{x|\phi \right\}=\left(\iota x|\phi \right)$$
7	6	eqeq2d	$$⊢\exists !x\phi \to \left(A=\bigcap \left\{x|\phi \right\}\leftrightarrow A=\left(\iota x|\phi \right)\right)$$
8		eqcom	$$⊢A=\left(\iota x|\phi \right)\leftrightarrow \left(\iota x|\phi \right)=A$$
9	1	iota2	$$⊢\left(A\in V\wedge \exists !x\phi \right)\to \left(\psi \leftrightarrow \left(\iota x|\phi \right)=A\right)$$
10	9	biimprd	$$⊢\left(A\in V\wedge \exists !x\phi \right)\to \left(\left(\iota x|\phi \right)=A\to \psi \right)$$
11	10	expcom	$$⊢\exists !x\phi \to \left(A\in V\to \left(\left(\iota x|\phi \right)=A\to \psi \right)\right)$$
12	11	com23	$$⊢\exists !x\phi \to \left(\left(\iota x|\phi \right)=A\to \left(A\in V\to \psi \right)\right)$$
13	8 12	biimtrid	$$⊢\exists !x\phi \to \left(A=\left(\iota x|\phi \right)\to \left(A\in V\to \psi \right)\right)$$
14	7 13	sylbid	$$⊢\exists !x\phi \to \left(A=\bigcap \left\{x|\phi \right\}\to \left(A\in V\to \psi \right)\right)$$
15	5 14	sylbid	$$⊢\exists !x\phi \to \left(A=if\left(\exists !x\phi ,\bigcap \left\{x|\phi \right\},\mathrm{V}\right)\to \left(A\in V\to \psi \right)\right)$$
16		iffalse	$$⊢\neg \exists !x\phi \to if\left(\exists !x\phi ,\bigcap \left\{x|\phi \right\},\mathrm{V}\right)=\mathrm{V}$$
17	16	eqeq2d	$$⊢\neg \exists !x\phi \to \left(A=if\left(\exists !x\phi ,\bigcap \left\{x|\phi \right\},\mathrm{V}\right)\leftrightarrow A=\mathrm{V}\right)$$
18		nvelim	$$⊢A=\mathrm{V}\to \neg A\in V$$
19	18	pm2.21d	$$⊢A=\mathrm{V}\to \left(A\in V\to \psi \right)$$
20	17 19	biimtrdi	$$⊢\neg \exists !x\phi \to \left(A=if\left(\exists !x\phi ,\bigcap \left\{x|\phi \right\},\mathrm{V}\right)\to \left(A\in V\to \psi \right)\right)$$
21	15 20	pm2.61i	$$⊢A=if\left(\exists !x\phi ,\bigcap \left\{x|\phi \right\},\mathrm{V}\right)\to \left(A\in V\to \psi \right)$$
22	3 21	sylbi	$$⊢A=\iota \to \left(A\in V\to \psi \right)$$
23	22	impcom	$$⊢\left(A\in V\wedge A=\iota \right)\to \psi$$