Definition df-1o 8501

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 8494	. 2 class 1o
2		c0 4281	. . 3 class ∅
3	2	csuc 6379	. 2 class suc ∅
4	1, 3	wceq 1570	1 wff 1o = suc ∅

This definition is used by:  df1o2  8508  1on  8514  1n0  8520  ordgt0ge1  8526  oa1suc  8564  o2p2e4  8574  om1  8575  oe1  8577  oelim2  8629  nnecl  8647  1onnALT  8675  omabs  8685  nnm1  8686  0sdom1domALT  9263  brttrcl2  9739  ssttrcl  9740  ttrcltr  9741  ttrclss  9745  dmttrcl  9746  rnttrcl  9747  ttrclselem2  9751  ackbij1lem14  10334  aleph1  10680  cfpwsdom  10693  nlt1pi  11015  indpi  11016  hash1  14572  aleph1re  16439  ltsval2  28040  ltssolem1  28059  nosepnelem  28063  nolt02o  28079  bday1  28227  cuteq1  28230  om2noseqlt  28712  bdaypw2n0bndlem  28876  bnj168  35428  r11  35806  gdlopcfv1  35971  satfv1  36294  fmla1  36318  rankeq1o  37109  finxp1o  38506  finxpreclem4  38508  finxp00  38516  ordeldif1o  44452  onov0suclim  44466  omabs2  44524  tfsconcatb0  44536  nlim1NEW  44633  aleph1min  44748  clsk1indlem1  45235