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

Definition df-8 8422
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 8413 . 2  class  8
2 c7 8412 . . 3  class  7
3 c1 7295 . . 3  class  1
4 caddc 7297 . . 3  class  +
52, 3, 4co 5613 . 2  class  ( 7  +  1 )
61, 5wceq 1287 1  wff  8  =  ( 7  +  1 )
Colors of variables: wff set class
This definition is referenced by:  8re  8442  8pos  8460  7p1e8  8489  4p4e8  8495  5p3e8  8497  6p2e8  8499  7p2e9  8501  8nn  8517  7lt8  8540  8p8e16  8894  9p8e17  8901  9p9e18  8902  8t8e64  8929  9t8e72  8936
  Copyright terms: Public domain W3C validator