Definition df-1o 8286

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 8279	. 2 class 1o
2		c0 4258	. . 3 class ∅
3	2	csuc 6263	. 2 class suc ∅
4	1, 3	wceq 1539	1 wff 1o = suc ∅

This definition is referenced by:  df1o2  8293  1on  8298  1onOLD  8299  ordgt0ge1  8312  oa1suc  8350  o2p2e4  8360  om1  8362  oe1  8364  oelim2  8415  nnecl  8433  1onnALT  8460  omabs  8470  nnm1  8471  0sdom1dom  9009  brttrcl2  9461  ssttrcl  9462  ttrcltr  9463  ttrclss  9467  dmttrcl  9468  rnttrcl  9469  ttrclselem2  9473  ackbij1lem14  9978  aleph1  10316  cfpwsdom  10329  nlt1pi  10651  indpi  10652  hash1  14108  aleph1re  15943  bnj168  32696  satfv1  33312  fmla1  33336  sltval2  33846  sltsolem1  33865  nosepnelem  33869  nolt02o  33885  bday1s  34012  rankeq1o  34460  finxp1o  35550  finxpreclem4  35552  finxp00  35560  aleph1min  41124  clsk1indlem1  41615