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

Definition df-1o 7048
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 7041 . 2  class  1o
2 c0 3711 . . 3  class  (/)
32csuc 4794 . 2  class  suc  (/)
41, 3wceq 1399 1  wff  1o  =  suc  (/)
Colors of variables: wff setvar class
This definition is referenced by:  1on  7055  df1o2  7060  ordgt0ge1  7065  oa1suc  7099  om1  7109  oe1  7111  oelim2  7162  nnecl  7180  1onn  7206  omabs  7214  nnm1  7215  0sdom1dom  7634  ackbij1lem14  8526  aleph1  8859  cfpwsdom  8872  nlt1pi  9195  indpi  9196  hash1  12373  aleph1re  13980  sltval2  29581  sltsolem1  29593  rankeq1o  29981  bnj168  34132  bj-1ex  34855
  Copyright terms: Public domain W3C validator