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

Definition df-7 8972
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 8964 . 2  class  7
2 c6 8963 . . 3  class  6
3 c1 7803 . . 3  class  1
4 caddc 7805 . . 3  class  +
52, 3, 4co 5869 . 2  class  ( 6  +  1 )
61, 5wceq 1353 1  wff  7  =  ( 6  +  1 )
Colors of variables: wff set class
This definition is referenced by:  7re  8991  7pos  9010  7m1e6  9032  6p1e7  9046  4p3e7  9052  5p2e7  9054  6p2e8  9057  7nn  9074  6lt7  9092  7p7e14  9451  8p7e15  9457  9p7e16  9464  9p8e17  9465  7t7e49  9486  8t7e56  9492  9t7e63  9499  lgsdir2lem3  14098
  Copyright terms: Public domain W3C validator