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

Metamath Proof Explorer

Theorem elsingles

Description: Membership in the class of all singletons. (Contributed by Scott Fenton, 19-Feb-2013)

Ref Expression
Assertion elsingles 
|- ( A e. Singletons <-> E. x A = { x } )

Proof

Step Hyp Ref Expression
1 elex 
 |-  ( A e. Singletons -> A e. _V )
2 vsnex 
 |-  { x } e. _V
3 eleq1 
 |-  ( A = { x } -> ( A e. _V <-> { x } e. _V ) )
4 2 3 mpbiri 
 |-  ( A = { x } -> A e. _V )
5 4 exlimiv 
 |-  ( E. x A = { x } -> A e. _V )
6 eleq1 
 |-  ( y = A -> ( y e. Singletons <-> A e. Singletons ) )
7 eqeq1 
 |-  ( y = A -> ( y = { x } <-> A = { x } ) )
8 7 exbidv 
 |-  ( y = A -> ( E. x y = { x } <-> E. x A = { x } ) )
9 df-singles 
 |-  Singletons = ran Singleton
10 9 eleq2i 
 |-  ( y e. Singletons <-> y e. ran Singleton )
11 vex 
 |-  y e. _V
12 11 elrn 
 |-  ( y e. ran Singleton <-> E. x x Singleton y )
13 vex 
 |-  x e. _V
14 13 11 brsingle 
 |-  ( x Singleton y <-> y = { x } )
15 14 exbii 
 |-  ( E. x x Singleton y <-> E. x y = { x } )
16 10 12 15 3bitri 
 |-  ( y e. Singletons <-> E. x y = { x } )
17 6 8 16 vtoclbg 
 |-  ( A e. _V -> ( A e. Singletons <-> E. x A = { x } ) )
18 1 5 17 pm5.21nii 
 |-  ( A e. Singletons <-> E. x A = { x } )