Metamath Proof Explorer


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 ( ∃! 𝑥𝐴 𝜑 ↔ ( 𝑥𝐴 𝜑 ) ∈ 𝐴 )