Theorem riotaclbgBAD

Description: Closure of restricted iota. (Contributed by NM, 28-Feb-2013) (Revised by Mario Carneiro, 24-Dec-2016)

	Ref	Expression
Assertion	riotaclbgBAD	$$⊢A\in V\to \left(\exists !x\in A\phi \leftrightarrow \left(\iota x\in A|\phi \right)\in A\right)$$

Proof

Step	Hyp	Ref	Expression
1		riotacl	$$⊢\exists !x\in A\phi \to \left(\iota x\in A|\phi \right)\in A$$
2		undefnel2	$$⊢A\in V\to \neg \mathrm{Undef}\left(A\right)\in A$$
3		iffalse	$$⊢\neg \exists !x\in A\phi \to if\left(\exists !x\in A\phi ,\left(\iota x|\left(x\in A\wedge \phi \right)\right),\mathrm{Undef}\left(\left\{x|x\in A\right\}\right)\right)=\mathrm{Undef}\left(\left\{x|x\in A\right\}\right)$$
4		ax-riotaBAD	$$⊢\left(\iota x\in A|\phi \right)=if\left(\exists !x\in A\phi ,\left(\iota x|\left(x\in A\wedge \phi \right)\right),\mathrm{Undef}\left(\left\{x|x\in A\right\}\right)\right)$$
5		abid1	$$⊢A=\left\{x|x\in A\right\}$$
6	5	fveq2i	$$⊢\mathrm{Undef}\left(A\right)=\mathrm{Undef}\left(\left\{x|x\in A\right\}\right)$$
7	3 4 6	3eqtr4g	$$⊢\neg \exists !x\in A\phi \to \left(\iota x\in A|\phi \right)=\mathrm{Undef}\left(A\right)$$
8	7	eleq1d	$$⊢\neg \exists !x\in A\phi \to \left(\left(\iota x\in A|\phi \right)\in A\leftrightarrow \mathrm{Undef}\left(A\right)\in A\right)$$
9	8	notbid	$$⊢\neg \exists !x\in A\phi \to \left(\neg \left(\iota x\in A|\phi \right)\in A\leftrightarrow \neg \mathrm{Undef}\left(A\right)\in A\right)$$
10	2 9	syl5ibrcom	$$⊢A\in V\to \left(\neg \exists !x\in A\phi \to \neg \left(\iota x\in A|\phi \right)\in A\right)$$
11	10	con4d	$$⊢A\in V\to \left(\left(\iota x\in A|\phi \right)\in A\to \exists !x\in A\phi \right)$$
12	1 11	impbid2	$$⊢A\in V\to \left(\exists !x\in A\phi \leftrightarrow \left(\iota x\in A|\phi \right)\in A\right)$$