This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem riotacl

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

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

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