MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-1o Structured version   Visualization version   GIF version

Definition df-1o 7520
Description: Define the ordinal number 1. (Contributed by NM, 29-Oct-1995.)
Assertion
Ref Expression
df-1o 1𝑜 = suc ∅

Detailed syntax breakdown of Definition df-1o
StepHypRef Expression
1 c1o 7513 . 2 class 1𝑜
2 c0 3897 . . 3 class
32csuc 5694 . 2 class suc ∅
41, 3wceq 1480 1 wff 1𝑜 = suc ∅
Colors of variables: wff setvar class
This definition is referenced by:  1on  7527  df1o2  7532  ordgt0ge1  7537  oa1suc  7571  om1  7582  oe1  7584  oelim2  7635  nnecl  7653  1onn  7679  omabs  7687  nnm1  7688  0sdom1dom  8118  ackbij1lem14  9015  aleph1  9353  cfpwsdom  9366  nlt1pi  9688  indpi  9689  hash1  13148  aleph1re  14918  bnj168  30559  sltval2  31563  sltsolem1  31581  nosepnelem  31618  rankeq1o  31973  bj-1ex  32638  finxp1o  32900  finxpreclem4  32902  finxp00  32910  clsk1indlem1  37864
  Copyright terms: Public domain W3C validator