Theorem cardsn

Description: A singleton has cardinality one. (Contributed by Mario Carneiro, 10-Jan-2013)

	Ref	Expression
Assertion	cardsn	|- ( A e. V -> ( card ` { A } ) = 1o )

Proof

Step	Hyp	Ref	Expression
1		eqid	|- { A } = { A }
2		sneq	|- ( x = A -> { x } = { A } )
3	2	eqeq2d	|- ( x = A -> ( { A } = { x } <-> { A } = { A } ) )
4	3	spcegv	|- ( A e. V -> ( { A } = { A } -> E. x { A } = { x } ) )
5	1 4	mpi	|- ( A e. V -> E. x { A } = { x } )
6		card1	|- ( ( card ` { A } ) = 1o <-> E. x { A } = { x } )
7	5 6	sylibr	|- ( A e. V -> ( card ` { A } ) = 1o )