Definition df-1o 8504

Description: Define the ordinal number 1. Definition 2.1 of [Schloeder] p. 4. (Contributed by NM, 29-Oct-1995.)

Assertion

Ref	Expression
df-1o	⊢ 1o = suc ∅

Detailed syntax breakdown of Definition df-1o

Step	Hyp	Ref	Expression
1		c1o 8497	. 2 class 1o
2		c0 4338	. . 3 class ∅
3	2	csuc 6387	. 2 class suc ∅
4	1, 3	wceq 1536	1 wff 1o = suc ∅

This definition is referenced by:  df1o2  8511  1on  8516  1onOLD  8517  ordgt0ge1  8529  oa1suc  8567  o2p2e4  8577  om1  8578  oe1  8580  oelim2  8631  nnecl  8649  1onnALT  8677  omabs  8687  nnm1  8688  0sdom1domALT  9272  brttrcl2  9751  ssttrcl  9752  ttrcltr  9753  ttrclss  9757  dmttrcl  9758  rnttrcl  9759  ttrclselem2  9763  ackbij1lem14  10269  aleph1  10608  cfpwsdom  10621  nlt1pi  10943  indpi  10944  hash1  14439  aleph1re  16277  sltval2  27715  sltsolem1  27734  nosepnelem  27738  nolt02o  27754  bday1s  27890  cuteq1  27892  om2noseqlt  28319  bnj168  34722  satfv1  35347  fmla1  35371  rankeq1o  36152  finxp1o  37374  finxpreclem4  37376  finxp00  37384  ordeldif1o  43249  onov0suclim  43263  omabs2  43321  tfsconcatb0  43333  nlim1NEW  43431  aleph1min  43546  clsk1indlem1  44034