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

Definition df-6 10018
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 10009 . 2  class  6
2 c5 10008 . . 3  class  5
3 c1 8947 . . 3  class  1
4 caddc 8949 . . 3  class  +
52, 3, 4co 6040 . 2  class  ( 5  +  1 )
61, 5wceq 1649 1  wff  6  =  ( 5  +  1 )
Colors of variables: wff set class
This definition is referenced by:  6re  10032  6pos  10044  5p1e6  10062  3p3e6  10068  4p2e6  10069  5p2e7  10072  6nn  10093  5lt6  10108  6p6e12  10389  7p6e13  10392  8p6e14  10397  8p8e16  10399  9p6e15  10404  9p7e16  10405  6t6e36  10419  7t6e42  10424  8t6e48  10430  9t6e54  10437  lt6abl  15459  ppiublem1  20939  ppiublem2  20940  ppiub  20941  bposlem8  21028  lgsdir2lem3  21062  rmydioph  26975  expdiophlem2  26983
  Copyright terms: Public domain W3C validator