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 7897
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
StepHypRef Expression
1 c1o 7890 . 2 class 1o
2 c0 4173 . . 3 class
32csuc 6025 . 2 class suc ∅
41, 3wceq 1507 1 wff 1o = suc ∅
Colors of variables: wff setvar class
This definition is referenced by:  1on  7904  df1o2  7910  ordgt0ge1  7916  oa1suc  7950  om1  7961  oe1  7963  oelim2  8014  nnecl  8032  1onn  8058  omabs  8066  nnm1  8067  0sdom1dom  8503  ackbij1lem14  9445  aleph1  9783  cfpwsdom  9796  nlt1pi  10118  indpi  10119  hash1  13569  aleph1re  15448  bnj168  31609  sltval2  32624  sltsolem1  32641  nosepnelem  32645  nolt02o  32660  rankeq1o  33093  finxp1o  34049  finxpreclem4  34051  finxp00  34059  clsk1indlem1  39703
  Copyright terms: Public domain W3C validator