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

Definition df-8 8055
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 8046 . 2  class  8
2 c7 8045 . . 3  class  7
3 c1 6948 . . 3  class  1
4 caddc 6950 . . 3  class  +
52, 3, 4co 5540 . 2  class  ( 7  +  1 )
61, 5wceq 1259 1  wff  8  =  ( 7  +  1 )
Colors of variables: wff set class
This definition is referenced by:  8re  8075  8pos  8093  7p1e8  8122  4p4e8  8128  5p3e8  8130  6p2e8  8132  7p2e9  8134  8nn  8150  7lt8  8173  8p8e16  8512  9p8e17  8519  9p9e18  8520  8t8e64  8547  9t8e72  8554
  Copyright terms: Public domain W3C validator