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

Definition df-4o 6004
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 5997 . 2  class  4o
2 c3o 5996 . . 3  class  3o
32csuc 4102 . 2  class  suc  3o
41, 3wceq 1243 1  wff  4o  =  suc  3o
Colors of variables: wff set class
This definition is referenced by:  4on  6012  4onn  6096
  Copyright terms: Public domain W3C validator