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

Definition df-1o 7193
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 7186 . 2  class  1o
2 c0 3761 . . 3  class  (/)
32csuc 5444 . 2  class  suc  (/)
41, 3wceq 1437 1  wff  1o  =  suc  (/)
Colors of variables: wff setvar class
This definition is referenced by:  1on  7200  df1o2  7205  ordgt0ge1  7210  oa1suc  7244  om1  7254  oe1  7256  oelim2  7307  nnecl  7325  1onn  7351  omabs  7359  nnm1  7360  0sdom1dom  7779  ackbij1lem14  8670  aleph1  9003  cfpwsdom  9016  nlt1pi  9338  indpi  9339  hash1  12587  aleph1re  14296  bnj168  29546  sltval2  30550  sltsolem1  30562  rankeq1o  30943  bj-1ex  31512  finxp1o  31748  finxpreclem4  31750  finxp00  31758
  Copyright terms: Public domain W3C validator