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

Definition df-1o 7169
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 7162 . 2  class  1o
2 c0 3699 . . 3  class  (/)
32csuc 5404 . 2  class  suc  (/)
41, 3wceq 1448 1  wff  1o  =  suc  (/)
Colors of variables: wff setvar class
This definition is referenced by:  1on  7176  df1o2  7181  ordgt0ge1  7186  oa1suc  7220  om1  7230  oe1  7232  oelim2  7283  nnecl  7301  1onn  7327  omabs  7335  nnm1  7336  0sdom1dom  7757  ackbij1lem14  8650  aleph1  8983  cfpwsdom  8996  nlt1pi  9318  indpi  9319  hash1  12575  aleph1re  14308  bnj168  29544  sltval2  30549  sltsolem1  30563  rankeq1o  30944  bj-1ex  31546  finxp1o  31786  finxpreclem4  31788  finxp00  31796
  Copyright terms: Public domain W3C validator