Definition df-1o 8522

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 8515	. 2 class 1o
2		c0 4352	. . 3 class ∅
3	2	csuc 6397	. 2 class suc ∅
4	1, 3	wceq 1537	1 wff 1o = suc ∅

This definition is referenced by:  df1o2  8529  1on  8534  1onOLD  8535  ordgt0ge1  8549  oa1suc  8587  o2p2e4  8597  om1  8598  oe1  8600  oelim2  8651  nnecl  8669  1onnALT  8697  omabs  8707  nnm1  8708  0sdom1domALT  9302  brttrcl2  9783  ssttrcl  9784  ttrcltr  9785  ttrclss  9789  dmttrcl  9790  rnttrcl  9791  ttrclselem2  9795  ackbij1lem14  10301  aleph1  10640  cfpwsdom  10653  nlt1pi  10975  indpi  10976  hash1  14453  aleph1re  16293  sltval2  27719  sltsolem1  27738  nosepnelem  27742  nolt02o  27758  bday1s  27894  cuteq1  27896  om2noseqlt  28323  bnj168  34706  satfv1  35331  fmla1  35355  rankeq1o  36135  finxp1o  37358  finxpreclem4  37360  finxp00  37368  ordeldif1o  43222  onov0suclim  43236  omabs2  43294  tfsconcatb0  43306  nlim1NEW  43404  aleph1min  43519  clsk1indlem1  44007