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

Definition df-7 8024
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 8015 . 2  class  7
2 c6 8014 . . 3  class  6
3 c1 6918 . . 3  class  1
4 caddc 6920 . . 3  class  +
52, 3, 4co 5537 . 2  class  ( 6  +  1 )
61, 5wceq 1257 1  wff  7  =  ( 6  +  1 )
Colors of variables: wff set class
This definition is referenced by:  7re  8043  7pos  8062  6p1e7  8091  4p3e7  8097  5p2e7  8099  6p2e8  8102  7nn  8119  6lt7  8137  7p7e14  8475  8p7e15  8481  9p7e16  8488  9p8e17  8489  7t7e49  8510  8t7e56  8516  9t7e63  8523
  Copyright terms: Public domain W3C validator