Definition df-1o 8391

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 8384	. 2 class 1o
2		c0 4282	. . 3 class ∅
3	2	csuc 6313	. 2 class suc ∅
4	1, 3	wceq 1541	1 wff 1o = suc ∅

This definition is referenced by:  df1o2  8398  1on  8403  ordgt0ge1  8414  oa1suc  8452  o2p2e4  8462  om1  8463  oe1  8465  oelim2  8516  nnecl  8534  1onnALT  8562  omabs  8572  nnm1  8573  0sdom1domALT  9138  brttrcl2  9611  ssttrcl  9612  ttrcltr  9613  ttrclss  9617  dmttrcl  9618  rnttrcl  9619  ttrclselem2  9623  ackbij1lem14  10130  aleph1  10469  cfpwsdom  10482  nlt1pi  10804  indpi  10805  hash1  14313  aleph1re  16156  sltval2  27596  sltsolem1  27615  nosepnelem  27619  nolt02o  27635  bday1s  27776  cuteq1  27779  om2noseqlt  28230  bnj168  34763  r11  35126  satfv1  35428  fmla1  35452  rankeq1o  36236  finxp1o  37457  finxpreclem4  37459  finxp00  37467  ordeldif1o  43377  onov0suclim  43391  omabs2  43449  tfsconcatb0  43461  nlim1NEW  43559  aleph1min  43674  clsk1indlem1  44162