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 ‘ 𝐴 ) = 1o ↔ ∃ 𝑥 𝐴 = { 𝑥 } )

Proof

Step	Hyp	Ref	Expression
1		1onn	⊢ 1o ∈ ω
2		cardnn	⊢ ( 1o ∈ ω → ( 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 ‘ 𝐴 ) ∧ ( card ‘ 1o ) ≠ ∅ ) → 1o ≈ 𝐴 )
7	5 6	mpan2	⊢ ( ( card ‘ 1o ) = ( card ‘ 𝐴 ) → 1o ≈ 𝐴 )
8	7	eqcoms	⊢ ( ( card ‘ 𝐴 ) = ( card ‘ 1o ) → 1o ≈ 𝐴 )
9	8	ensymd	⊢ ( ( card ‘ 𝐴 ) = ( card ‘ 1o ) → 𝐴 ≈ 1o )
10		carden2b	⊢ ( 𝐴 ≈ 1o → ( card ‘ 𝐴 ) = ( card ‘ 1o ) )
11	9 10	impbii	⊢ ( ( card ‘ 𝐴 ) = ( card ‘ 1o ) ↔ 𝐴 ≈ 1o )
12	3	eqeq2i	⊢ ( ( card ‘ 𝐴 ) = ( card ‘ 1o ) ↔ ( card ‘ 𝐴 ) = 1o )
13		en1	⊢ ( 𝐴 ≈ 1o ↔ ∃ 𝑥 𝐴 = { 𝑥 } )
14	11 12 13	3bitr3i	⊢ ( ( card ‘ 𝐴 ) = 1o ↔ ∃ 𝑥 𝐴 = { 𝑥 } )