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

Definition df-1o 6908
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 6901 . 2  class  1o
2 c0 3625 . . 3  class  (/)
32csuc 4708 . 2  class  suc  (/)
41, 3wceq 1362 1  wff  1o  =  suc  (/)
Colors of variables: wff setvar class
This definition is referenced by:  1on  6915  df1o2  6920  ordgt0ge1  6925  oa1suc  6959  om1  6969  oe1  6971  oelim2  7022  nnecl  7040  1onn  7066  omabs  7074  nnm1  7075  0sdom1dom  7498  ackbij1lem14  8390  aleph1  8723  cfpwsdom  8736  nlt1pi  9063  indpi  9064  hash1  12146  aleph1re  13510  sltval2  27644  sltsolem1  27656  rankeq1o  28056  bnj168  31444  bj-1ex  32046
  Copyright terms: Public domain W3C validator