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

Definition df-8 9049
Description: Define the number 8. (Contributed by NM, 27-May-1999.)
Assertion
Ref Expression
df-8  |-  8  =  ( 7  +  1 )

Detailed syntax breakdown of Definition df-8
StepHypRef Expression
1 c8 9041 . 2  class  8
2 c7 9040 . . 3  class  7
3 c1 7875 . . 3  class  1
4 caddc 7877 . . 3  class  +
52, 3, 4co 5919 . 2  class  ( 7  +  1 )
61, 5wceq 1364 1  wff  8  =  ( 7  +  1 )
Colors of variables: wff set class
This definition is referenced by:  8re  9069  8pos  9087  8m1e7  9109  7p1e8  9124  4p4e8  9130  5p3e8  9132  6p2e8  9134  7p2e9  9136  8nn  9152  7lt8  9175  8p8e16  9536  9p8e17  9543  9p9e18  9544  8t8e64  9571  9t8e72  9578
  Copyright terms: Public domain W3C validator