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

Definition df-7 8424
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 8415 . 2  class  7
2 c6 8414 . . 3  class  6
3 c1 7298 . . 3  class  1
4 caddc 7300 . . 3  class  +
52, 3, 4co 5615 . 2  class  ( 6  +  1 )
61, 5wceq 1287 1  wff  7  =  ( 6  +  1 )
Colors of variables: wff set class
This definition is referenced by:  7re  8443  7pos  8462  6p1e7  8491  4p3e7  8497  5p2e7  8499  6p2e8  8502  7nn  8519  6lt7  8537  7p7e14  8890  8p7e15  8896  9p7e16  8903  9p8e17  8904  7t7e49  8925  8t7e56  8931  9t7e63  8938
  Copyright terms: Public domain W3C validator