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

Metamath Proof Explorer

Theorem sniota

Description: A class abstraction with a unique member can be expressed as a singleton. (Contributed by Mario Carneiro, 23-Dec-2016)

Ref Expression
Assertion sniota 
|- ( E! x ph -> { x | ph } = { ( iota x ph ) } )

Proof

Step Hyp Ref Expression
1 nfeu1 
 |-  F/ x E! x ph
2 nfab1 
 |-  F/_ x { x | ph }
3 nfiota1 
 |-  F/_ x ( iota x ph )
4 3 nfsn 
 |-  F/_ x { ( iota x ph ) }
5 iota1 
 |-  ( E! x ph -> ( ph <-> ( iota x ph ) = x ) )
6 eqcom 
 |-  ( ( iota x ph ) = x <-> x = ( iota x ph ) )
7 5 6 bitrdi 
 |-  ( E! x ph -> ( ph <-> x = ( iota x ph ) ) )
8 abid 
 |-  ( x e. { x | ph } <-> ph )
9 velsn 
 |-  ( x e. { ( iota x ph ) } <-> x = ( iota x ph ) )
10 7 8 9 3bitr4g 
 |-  ( E! x ph -> ( x e. { x | ph } <-> x e. { ( iota x ph ) } ) )
11 1 2 4 10 eqrd 
 |-  ( E! x ph -> { x | ph } = { ( iota x ph ) } )