Definition df-1o 8180

Description: Define the ordinal number 1. (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 8173	. 2 class 1o
2		c0 4223	. . 3 class ∅
3	2	csuc 6193	. 2 class suc ∅
4	1, 3	wceq 1543	1 wff 1o = suc ∅

This definition is referenced by:  1on  8187  df1o2  8192  ordgt0ge1  8202  oa1suc  8236  o2p2e4  8246  om1  8248  oe1  8250  oelim2  8301  nnecl  8319  1onn  8345  omabs  8354  nnm1  8355  0sdom1dom  8852  ackbij1lem14  9812  aleph1  10150  cfpwsdom  10163  nlt1pi  10485  indpi  10486  hash1  13936  aleph1re  15769  bnj168  32375  satfv1  32992  fmla1  33016  sltval2  33545  sltsolem1  33564  nosepnelem  33568  nolt02o  33584  bday1s  33711  rankeq1o  34159  finxp1o  35249  finxpreclem4  35251  finxp00  35259  aleph1min  40781  clsk1indlem1  41273