Theorem card1

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

	Ref	Expression
Assertion	card1	$$⊢\mathrm{card}\left(A\right)=1_{𝑜}\leftrightarrow \exists xA=\left\{x\right\}$$

Proof

Step	Hyp	Ref	Expression
1		1onn	$$⊢1_{𝑜}\in \mathrm{\omega }$$
2		cardnn	$$⊢1_{𝑜}\in \mathrm{\omega }\to \mathrm{card}\left(1_{𝑜}\right)=1_{𝑜}$$
3	1 2	ax-mp	$$⊢\mathrm{card}\left(1_{𝑜}\right)=1_{𝑜}$$
4		1n0	$$⊢1_{𝑜}\ne \varnothing$$
5	3 4	eqnetri	$$⊢\mathrm{card}\left(1_{𝑜}\right)\ne \varnothing$$
6		carden2a	$$⊢\left(\mathrm{card}\left(1_{𝑜}\right)=\mathrm{card}\left(A\right)\wedge \mathrm{card}\left(1_{𝑜}\right)\ne \varnothing \right)\to 1_{𝑜}\approx A$$
7	5 6	mpan2	$$⊢\mathrm{card}\left(1_{𝑜}\right)=\mathrm{card}\left(A\right)\to 1_{𝑜}\approx A$$
8	7	eqcoms	$$⊢\mathrm{card}\left(A\right)=\mathrm{card}\left(1_{𝑜}\right)\to 1_{𝑜}\approx A$$
9	8	ensymd	$$⊢\mathrm{card}\left(A\right)=\mathrm{card}\left(1_{𝑜}\right)\to A\approx 1_{𝑜}$$
10		carden2b	$$⊢A\approx 1_{𝑜}\to \mathrm{card}\left(A\right)=\mathrm{card}\left(1_{𝑜}\right)$$
11	9 10	impbii	$$⊢\mathrm{card}\left(A\right)=\mathrm{card}\left(1_{𝑜}\right)\leftrightarrow A\approx 1_{𝑜}$$
12	3	eqeq2i	$$⊢\mathrm{card}\left(A\right)=\mathrm{card}\left(1_{𝑜}\right)\leftrightarrow \mathrm{card}\left(A\right)=1_{𝑜}$$
13		en1	$$⊢A\approx 1_{𝑜}\leftrightarrow \exists xA=\left\{x\right\}$$
14	11 12 13	3bitr3i	$$⊢\mathrm{card}\left(A\right)=1_{𝑜}\leftrightarrow \exists xA=\left\{x\right\}$$