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

Definition df-1o 6495
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 6488 . 2  class  1o
2 c0 3468 . . 3  class  (/)
32csuc 4410 . 2  class  suc  (/)
41, 3wceq 1632 1  wff  1o  =  suc  (/)
Colors of variables: wff set class
This definition is referenced by:  1on  6502  df1o2  6507  ordgt0ge1  6512  oa1suc  6546  om1  6556  oe1  6558  oelim2  6609  nnecl  6627  1onn  6653  omabs  6661  nnm1  6662  0sdom1dom  7076  ackbij1lem14  7875  aleph1  8209  cfpwsdom  8222  nlt1pi  8546  indpi  8547  hash1  11386  aleph1re  12539  sltval2  24381  sltsolem1  24393  rankeq1o  24873  bnj168  29074
  Copyright terms: Public domain W3C validator