Theorem riotaclbBAD

Description: Closure of restricted iota. (Contributed by NM, 15-Sep-2011)

	Ref	Expression
Hypothesis	riotaclb.1	⊢ 𝐴 ∈ V
Assertion	riotaclbBAD	⊢ ( ∃! 𝑥 ∈ 𝐴 𝜑 ↔ ( ℩ 𝑥 ∈ 𝐴 𝜑 ) ∈ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		riotaclb.1	⊢ 𝐴 ∈ V
2		riotaclbgBAD	⊢ ( 𝐴 ∈ V → ( ∃! 𝑥 ∈ 𝐴 𝜑 ↔ ( ℩ 𝑥 ∈ 𝐴 𝜑 ) ∈ 𝐴 ) )
3	1 2	ax-mp	⊢ ( ∃! 𝑥 ∈ 𝐴 𝜑 ↔ ( ℩ 𝑥 ∈ 𝐴 𝜑 ) ∈ 𝐴 )