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	⊢ ( ℩ 𝑥 ∈ 𝐴 𝜑 ) ⊆ ( 𝒫 ∪ 𝐴 ∪ ∪ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		riotauni	⊢ ( ∃! 𝑥 ∈ 𝐴 𝜑 → ( ℩ 𝑥 ∈ 𝐴 𝜑 ) = ∪ { 𝑥 ∈ 𝐴 ∣ 𝜑 } )
2		ssrab2	⊢ { 𝑥 ∈ 𝐴 ∣ 𝜑 } ⊆ 𝐴
3	2	unissi	⊢ ∪ { 𝑥 ∈ 𝐴 ∣ 𝜑 } ⊆ ∪ 𝐴
4		ssun2	⊢ ∪ 𝐴 ⊆ ( 𝒫 ∪ 𝐴 ∪ ∪ 𝐴 )
5	3 4	sstri	⊢ ∪ { 𝑥 ∈ 𝐴 ∣ 𝜑 } ⊆ ( 𝒫 ∪ 𝐴 ∪ ∪ 𝐴 )
6	1 5	eqsstrdi	⊢ ( ∃! 𝑥 ∈ 𝐴 𝜑 → ( ℩ 𝑥 ∈ 𝐴 𝜑 ) ⊆ ( 𝒫 ∪ 𝐴 ∪ ∪ 𝐴 ) )
7		riotaund	⊢ ( ¬ ∃! 𝑥 ∈ 𝐴 𝜑 → ( ℩ 𝑥 ∈ 𝐴 𝜑 ) = ∅ )
8		0ss	⊢ ∅ ⊆ ( 𝒫 ∪ 𝐴 ∪ ∪ 𝐴 )
9	7 8	eqsstrdi	⊢ ( ¬ ∃! 𝑥 ∈ 𝐴 𝜑 → ( ℩ 𝑥 ∈ 𝐴 𝜑 ) ⊆ ( 𝒫 ∪ 𝐴 ∪ ∪ 𝐴 ) )
10	6 9	pm2.61i	⊢ ( ℩ 𝑥 ∈ 𝐴 𝜑 ) ⊆ ( 𝒫 ∪ 𝐴 ∪ ∪ 𝐴 )