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