Theorem riotaclb

Description: Bidirectional closure of restricted iota when domain is not empty. (Contributed by NM, 28-Feb-2013) (Revised by Mario Carneiro, 24-Dec-2016) (Revised by NM, 13-Sep-2018)

	Ref	Expression
Assertion	riotaclb	$$⊢\neg \varnothing \in A\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		riotaund	$$⊢\neg \exists !x\in A\phi \to \left(\iota x\in A|\phi \right)=\varnothing$$
3	2	eleq1d	$$⊢\neg \exists !x\in A\phi \to \left(\left(\iota x\in A|\phi \right)\in A\leftrightarrow \varnothing \in A\right)$$
4	3	notbid	$$⊢\neg \exists !x\in A\phi \to \left(\neg \left(\iota x\in A|\phi \right)\in A\leftrightarrow \neg \varnothing \in A\right)$$
5	4	biimprcd	$$⊢\neg \varnothing \in A\to \left(\neg \exists !x\in A\phi \to \neg \left(\iota x\in A|\phi \right)\in A\right)$$
6	5	con4d	$$⊢\neg \varnothing \in A\to \left(\left(\iota x\in A|\phi \right)\in A\to \exists !x\in A\phi \right)$$
7	1 6	impbid2	$$⊢\neg \varnothing \in A\to \left(\exists !x\in A\phi \leftrightarrow \left(\iota x\in A|\phi \right)\in A\right)$$