Definition df-1o 8439

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 8432	. 2 class 1o
2		c0 4287	. . 3 class ∅
3	2	csuc 6350	. 2 class suc ∅
4	1, 3	wceq 1562	1 wff 1o = suc ∅

This definition is referenced by:  df1o2  8446  1on  8452  1n0  8458  ordgt0ge1  8464  oa1suc  8502  o2p2e4  8512  om1  8513  oe1  8515  oelim2  8567  nnecl  8585  1onnALT  8613  omabs  8623  nnm1  8624  0sdom1domALT  9193  brttrcl2  9671  ssttrcl  9672  ttrcltr  9673  ttrclss  9677  dmttrcl  9678  rnttrcl  9679  ttrclselem2  9683  ackbij1lem14  10190  aleph1  10531  cfpwsdom  10544  nlt1pi  10866  indpi  10867  hash1  14419  aleph1re  16279  ltsval2  27722  ltssolem1  27741  nosepnelem  27745  nolt02o  27761  bday1  27909  cuteq1  27912  om2noseqlt  28394  bdaypw2n0bndlem  28558  bnj168  35028  r11  35394  satfv1  35718  fmla1  35742  rankeq1o  36526  finxp1o  37891  finxpreclem4  37893  finxp00  37901  ordeldif1o  43842  onov0suclim  43856  omabs2  43914  tfsconcatb0  43926  nlim1NEW  44023  aleph1min  44138  clsk1indlem1  44626