Theorem riotaund

Description: Restricted iota equals the empty set when not meaningful. (Contributed by NM, 16-Jan-2012) (Revised by Mario Carneiro, 15-Oct-2016) (Revised by NM, 13-Sep-2018)

	Ref	Expression
Assertion	riotaund	$$⊢\neg \exists !x\in A\phi \to \left(\iota x\in A|\phi \right)=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		df-riota	$$⊢\left(\iota x\in A|\phi \right)=\left(\iota x|\left(x\in A\wedge \phi \right)\right)$$
2		df-reu	$$⊢\exists !x\in A\phi \leftrightarrow \exists !x\left(x\in A\wedge \phi \right)$$
3		iotanul	$$⊢\neg \exists !x\left(x\in A\wedge \phi \right)\to \left(\iota x|\left(x\in A\wedge \phi \right)\right)=\varnothing$$
4	2 3	sylnbi	$$⊢\neg \exists !x\in A\phi \to \left(\iota x|\left(x\in A\wedge \phi \right)\right)=\varnothing$$
5	1 4	syl5eq	$$⊢\neg \exists !x\in A\phi \to \left(\iota x\in A|\phi \right)=\varnothing$$