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

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

Detailed syntax breakdown of Definition df-4o
StepHypRef Expression
1 c4o 6475 . 2  class  4o
2 c3o 6474 . . 3  class  3o
32csuc 4394 . 2  class  suc  3o
41, 3wceq 1623 1  wff  4o  =  suc  3o
Colors of variables: wff set class
This definition is referenced by:  4on  6490  4onn  6640  en4  7096  hash4  11373
  Copyright terms: Public domain W3C validator