ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-4o Unicode version

Definition df-4o 6323
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 6316 . 2  class  4o
2 c3o 6315 . . 3  class  3o
32csuc 4294 . 2  class  suc  3o
41, 3wceq 1332 1  wff  4o  =  suc  3o
Colors of variables: wff set class
This definition is referenced by:  4on  6332  4onn  6426  hash4  10591
  Copyright terms: Public domain W3C validator