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

Definition df-7 8688
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 8680 . 2  class  7
2 c6 8679 . . 3  class  6
3 c1 7542 . . 3  class  1
4 caddc 7544 . . 3  class  +
52, 3, 4co 5726 . 2  class  ( 6  +  1 )
61, 5wceq 1312 1  wff  7  =  ( 6  +  1 )
Colors of variables: wff set class
This definition is referenced by:  7re  8707  7pos  8726  6p1e7  8756  4p3e7  8762  5p2e7  8764  6p2e8  8767  7nn  8784  6lt7  8802  7p7e14  9158  8p7e15  9164  9p7e16  9171  9p8e17  9172  7t7e49  9193  8t7e56  9199  9t7e63  9206
  Copyright terms: Public domain W3C validator