Metamath Proof Explorer


Theorem snriota

Description: A restricted class abstraction with a unique member can be expressed as a singleton. (Contributed by NM, 30-May-2006)

Ref Expression
Assertion snriota ∃!xAφxA|φ=ιxA|φ

Proof

Step Hyp Ref Expression
1 df-reu ∃!xAφ∃!xxAφ
2 sniota ∃!xxAφx|xAφ=ιx|xAφ
3 1 2 sylbi ∃!xAφx|xAφ=ιx|xAφ
4 df-rab xA|φ=x|xAφ
5 df-riota ιxA|φ=ιx|xAφ
6 5 sneqi ιxA|φ=ιx|xAφ
7 3 4 6 3eqtr4g ∃!xAφxA|φ=ιxA|φ