Theorem ensn1

Description: A singleton is equinumerous to ordinal one. (Contributed by NM, 4-Nov-2002)

	Ref	Expression
Hypothesis	ensn1.1	|- A e. _V
Assertion	ensn1	|- { A } ~~ 1o

Proof

Step	Hyp	Ref	Expression
1		ensn1.1	|- A e. _V
2		snex	|- { <. A , (/) >. } e. _V
3		f1oeq1	|- ( f = { <. A , (/) >. } -> ( f : { A } -1-1-onto-> { (/) } <-> { <. A , (/) >. } : { A } -1-1-onto-> { (/) } ) )
4		0ex	|- (/) e. _V
5	1 4	f1osn	|- { <. A , (/) >. } : { A } -1-1-onto-> { (/) }
6	2 3 5	ceqsexv2d	|- E. f f : { A } -1-1-onto-> { (/) }
7		bren	|- ( { A } ~~ { (/) } <-> E. f f : { A } -1-1-onto-> { (/) } )
8	6 7	mpbir	|- { A } ~~ { (/) }
9		df1o2	|- 1o = { (/) }
10	8 9	breqtrri	|- { A } ~~ 1o