MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-6 Unicode version

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

Detailed syntax breakdown of Definition df-6
StepHypRef Expression
1 c6 9844 . 2  class  6
2 c5 9843 . . 3  class  5
3 c1 8783 . . 3  class  1
4 caddc 8785 . . 3  class  +
52, 3, 4co 5900 . 2  class  ( 5  +  1 )
61, 5wceq 1633 1  wff  6  =  ( 5  +  1 )
Colors of variables: wff set class
This definition is referenced by:  6re  9867  6pos  9879  5p1e6  9897  3p3e6  9903  4p2e6  9904  5p2e7  9907  6nn  9928  5lt6  9943  6p6e12  10222  7p6e13  10225  8p6e14  10230  8p8e16  10232  9p6e15  10237  9p7e16  10238  6t6e36  10252  7t6e42  10257  8t6e48  10263  9t6e54  10270  lt6abl  15230  ppiublem1  20494  ppiublem2  20495  ppiub  20496  bposlem8  20583  lgsdir2lem3  20617  rmydioph  26255  expdiophlem2  26263
  Copyright terms: Public domain W3C validator