Definition df-1o 8476

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 8469	. 2 class 1o
2		c0 4278	. . 3 class ∅
3	2	csuc 6364	. 2 class suc ∅
4	1, 3	wceq 1569	1 wff 1o = suc ∅

This definition is used by:  df1o2  8483  1on  8489  1n0  8495  ordgt0ge1  8501  oa1suc  8539  o2p2e4  8549  om1  8550  oe1  8552  oelim2  8604  nnecl  8622  1onnALT  8650  omabs  8660  nnm1  8661  0sdom1domALT  9238  brttrcl2  9715  ssttrcl  9716  ttrcltr  9717  ttrclss  9721  dmttrcl  9722  rnttrcl  9723  ttrclselem2  9727  ackbij1lem14  10310  aleph1  10656  cfpwsdom  10669  nlt1pi  10991  indpi  10992  hash1  14548  aleph1re  16413  ltsval2  28013  ltssolem1  28032  nosepnelem  28036  nolt02o  28052  bday1  28200  cuteq1  28203  om2noseqlt  28685  bdaypw2n0bndlem  28849  bnj168  35403  r11  35767  satfv1  36170  fmla1  36194  rankeq1o  36974  finxp1o  38358  finxpreclem4  38360  finxp00  38368  ordeldif1o  44304  onov0suclim  44318  omabs2  44376  tfsconcatb0  44388  nlim1NEW  44485  aleph1min  44600  clsk1indlem1  45087