Theorem riotacl

Description: Closure of restricted iota. (Contributed by NM, 21-Aug-2011)

	Ref	Expression
Assertion	riotacl	⊢ ( ∃! 𝑥 ∈ 𝐴 𝜑 → ( ℩ 𝑥 ∈ 𝐴 𝜑 ) ∈ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		ssrab2	⊢ { 𝑥 ∈ 𝐴 ∣ 𝜑 } ⊆ 𝐴
2		riotacl2	⊢ ( ∃! 𝑥 ∈ 𝐴 𝜑 → ( ℩ 𝑥 ∈ 𝐴 𝜑 ) ∈ { 𝑥 ∈ 𝐴 ∣ 𝜑 } )
3	1 2	sseldi	⊢ ( ∃! 𝑥 ∈ 𝐴 𝜑 → ( ℩ 𝑥 ∈ 𝐴 𝜑 ) ∈ 𝐴 )