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

Definition df-8 8960
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 8952 . 2  class  8
2 c7 8951 . . 3  class  7
3 c1 7790 . . 3  class  1
4 caddc 7792 . . 3  class  +
52, 3, 4co 5868 . 2  class  ( 7  +  1 )
61, 5wceq 1353 1  wff  8  =  ( 7  +  1 )
Colors of variables: wff set class
This definition is referenced by:  8re  8980  8pos  8998  8m1e7  9020  7p1e8  9034  4p4e8  9040  5p3e8  9042  6p2e8  9044  7p2e9  9046  8nn  9062  7lt8  9085  8p8e16  9445  9p8e17  9452  9p9e18  9453  8t8e64  9480  9t8e72  9487
  Copyright terms: Public domain W3C validator