Theorem riotassuni

Description: The restricted iota class is limited in size by the base set. (Contributed by Mario Carneiro, 24-Dec-2016)

	Ref	Expression
Assertion	riotassuni	$$⊢\left(\iota x\in A|\phi \right)\subseteq 𝒫\bigcup A\cup \bigcup A$$

Proof

Step	Hyp	Ref	Expression
1		riotauni	$$⊢\exists !x\in A\phi \to \left(\iota x\in A|\phi \right)=\bigcup \left\{x\in A|\phi \right\}$$
2		ssrab2	$$⊢\left\{x\in A|\phi \right\}\subseteq A$$
3	2	unissi	$$⊢\bigcup \left\{x\in A|\phi \right\}\subseteq \bigcup A$$
4		ssun2	$$⊢\bigcup A\subseteq 𝒫\bigcup A\cup \bigcup A$$
5	3 4	sstri	$$⊢\bigcup \left\{x\in A|\phi \right\}\subseteq 𝒫\bigcup A\cup \bigcup A$$
6	1 5	eqsstrdi	$$⊢\exists !x\in A\phi \to \left(\iota x\in A|\phi \right)\subseteq 𝒫\bigcup A\cup \bigcup A$$
7		riotaund	$$⊢\neg \exists !x\in A\phi \to \left(\iota x\in A|\phi \right)=\varnothing$$
8		0ss	$$⊢\varnothing \subseteq 𝒫\bigcup A\cup \bigcup A$$
9	7 8	eqsstrdi	$$⊢\neg \exists !x\in A\phi \to \left(\iota x\in A|\phi \right)\subseteq 𝒫\bigcup A\cup \bigcup A$$
10	6 9	pm2.61i	$$⊢\left(\iota x\in A|\phi \right)\subseteq 𝒫\bigcup A\cup \bigcup A$$