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

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

Detailed syntax breakdown of Definition df-5
StepHypRef Expression
1 c5 9766 . 2  class  5
2 c4 9765 . . 3  class  4
3 c1 8706 . . 3  class  1
4 caddc 8708 . . 3  class  +
52, 3, 4co 5792 . 2  class  ( 4  +  1 )
61, 5wceq 1619 1  wff  5  =  ( 4  +  1 )
Colors of variables: wff set class
This definition is referenced by:  5re  9789  5pos  9801  4p1e5  9817  3p2e5  9823  4p2e6  9825  5p5e10  9831  5nn  9848  4lt5  9860  6p5e11  10142  7p5e12  10145  8p5e13  10150  8p7e15  10152  9p5e14  10157  9p6e15  10158  5t5e25  10168  6t5e30  10172  7t5e35  10177  8t5e40  10183  9t5e45  10190  ef01bndlem  12427  5prm  13073  lt6abl  15144  log2ublem3  20207  ppiublem2  20405  bclbnd  20482  bposlem6  20491  bposlem9  20494  lgsdir2lem3  20527  rmydioph  26475  expdiophlem2  26483  stoweidlem13  27131
  Copyright terms: Public domain W3C validator