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

Definition df-6 9803
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 9794 . 2  class  6
2 c5 9793 . . 3  class  5
3 c1 8733 . . 3  class  1
4 caddc 8735 . . 3  class  +
52, 3, 4co 5819 . 2  class  ( 5  +  1 )
61, 5wceq 1624 1  wff  6  =  ( 5  +  1 )
Colors of variables: wff set class
This definition is referenced by:  6re  9817  6pos  9829  5p1e6  9845  3p3e6  9851  4p2e6  9852  5p2e7  9855  6nn  9876  5lt6  9891  6p6e12  10170  7p6e13  10173  8p6e14  10178  8p8e16  10180  9p6e15  10185  9p7e16  10186  6t6e36  10200  7t6e42  10205  8t6e48  10211  9t6e54  10218  lt6abl  15175  ppiublem1  20435  ppiublem2  20436  ppiub  20437  bposlem8  20524  lgsdir2lem3  20558  rmydioph  26506  expdiophlem2  26514
  Copyright terms: Public domain W3C validator