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

Metamath Proof Explorer

Theorem card1

Description: A set has cardinality one iff it is a singleton. (Contributed by Mario Carneiro, 10-Jan-2013)

Ref Expression
Assertion card1 
|- ( ( card ` A ) = 1o <-> E. x A = { x } )

Proof

Step Hyp Ref Expression
1 1onn 
 |-  1o e. _om
2 cardnn 
 |-  ( 1o e. _om -> ( card ` 1o ) = 1o )
3 1 2 ax-mp 
 |-  ( card ` 1o ) = 1o
4 1n0 
 |-  1o =/= (/)
5 3 4 eqnetri 
 |-  ( card ` 1o ) =/= (/)
6 carden2a 
 |-  ( ( ( card ` 1o ) = ( card ` A ) /\ ( card ` 1o ) =/= (/) ) -> 1o ~~ A )
7 5 6 mpan2 
 |-  ( ( card ` 1o ) = ( card ` A ) -> 1o ~~ A )
8 7 eqcoms 
 |-  ( ( card ` A ) = ( card ` 1o ) -> 1o ~~ A )
9 8 ensymd 
 |-  ( ( card ` A ) = ( card ` 1o ) -> A ~~ 1o )
10 carden2b 
 |-  ( A ~~ 1o -> ( card ` A ) = ( card ` 1o ) )
11 9 10 impbii 
 |-  ( ( card ` A ) = ( card ` 1o ) <-> A ~~ 1o )
12 3 eqeq2i 
 |-  ( ( card ` A ) = ( card ` 1o ) <-> ( card ` A ) = 1o )
13 en1 
 |-  ( A ~~ 1o <-> E. x A = { x } )
14 11 12 13 3bitr3i 
 |-  ( ( card ` A ) = 1o <-> E. x A = { x } )