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

Definition df-1o 7190
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 7183 . 2  class  1o
2 c0 3767 . . 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  7197  df1o2  7202  ordgt0ge1  7207  oa1suc  7241  om1  7251  oe1  7253  oelim2  7304  nnecl  7322  1onn  7348  omabs  7356  nnm1  7357  0sdom1dom  7776  ackbij1lem14  8661  aleph1  8994  cfpwsdom  9007  nlt1pi  9330  indpi  9331  hash1  12578  aleph1re  14275  bnj168  29326  sltval2  30330  sltsolem1  30342  rankeq1o  30723  bj-1ex  31293
  Copyright terms: Public domain W3C validator