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

Definition df-3o 8415
Description: Define the ordinal number 3. (Contributed by Mario Carneiro, 14-Jul-2013.)
Assertion
Ref Expression
df-3o 3o = suc 2o

Detailed syntax breakdown of Definition df-3o
StepHypRef Expression
1 c3o 8408 . 2 class 3o
2 c2o 8407 . . 3 class 2o
32csuc 6320 . 2 class suc 2o
41, 3wceq 1542 1 wff 3o = suc 2o
Colors of variables: wff setvar class
This definition is referenced by:  ord3  8430  3on  8431  o2p2e4  8488  o2p2e4OLD  8489  3onn  8591  en3  9227  hash3  14307  finxp3o  35874  df3o2  41650  df3o3  41651  omcl3g  41670  nlim3  41723  tr3dom  41807  har2o  41825  clsk1independent  42325
  Copyright terms: Public domain W3C validator