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

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

Detailed syntax breakdown of Definition df-7
StepHypRef Expression
1 c7 8161 . 2  class  7
2 c6 8160 . . 3  class  6
3 c1 7044 . . 3  class  1
4 caddc 7046 . . 3  class  +
52, 3, 4co 5543 . 2  class  ( 6  +  1 )
61, 5wceq 1285 1  wff  7  =  ( 6  +  1 )
Colors of variables: wff set class
This definition is referenced by:  7re  8189  7pos  8208  6p1e7  8237  4p3e7  8243  5p2e7  8245  6p2e8  8248  7nn  8265  6lt7  8283  7p7e14  8636  8p7e15  8642  9p7e16  8649  9p8e17  8650  7t7e49  8671  8t7e56  8677  9t7e63  8684
  Copyright terms: Public domain W3C validator