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

Definition df-8 8808
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 8800 . 2  class  8
2 c7 8799 . . 3  class  7
3 c1 7644 . . 3  class  1
4 caddc 7646 . . 3  class  +
52, 3, 4co 5781 . 2  class  ( 7  +  1 )
61, 5wceq 1332 1  wff  8  =  ( 7  +  1 )
Colors of variables: wff set class
This definition is referenced by:  8re  8828  8pos  8846  8m1e7  8868  7p1e8  8882  4p4e8  8888  5p3e8  8890  6p2e8  8892  7p2e9  8894  8nn  8910  7lt8  8933  8p8e16  9290  9p8e17  9297  9p9e18  9298  8t8e64  9325  9t8e72  9332
  Copyright terms: Public domain W3C validator