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
|- ( E! x e. A ph -> { x e. A | ph } = { ( iota_ x e. A ph ) } )

Proof

Step Hyp Ref Expression
1 df-reu
 |-  ( E! x e. A ph <-> E! x ( x e. A /\ ph ) )
2 sniota
 |-  ( E! x ( x e. A /\ ph ) -> { x | ( x e. A /\ ph ) } = { ( iota x ( x e. A /\ ph ) ) } )
3 1 2 sylbi
 |-  ( E! x e. A ph -> { x | ( x e. A /\ ph ) } = { ( iota x ( x e. A /\ ph ) ) } )
4 df-rab
 |-  { x e. A | ph } = { x | ( x e. A /\ ph ) }
5 df-riota
 |-  ( iota_ x e. A ph ) = ( iota x ( x e. A /\ ph ) )
6 5 sneqi
 |-  { ( iota_ x e. A ph ) } = { ( iota x ( x e. A /\ ph ) ) }
7 3 4 6 3eqtr4g
 |-  ( E! x e. A ph -> { x e. A | ph } = { ( iota_ x e. A ph ) } )