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 } )