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

Definition df-5 9740
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 9731 . 2  class  5
2 c4 9730 . . 3  class  4
3 c1 8671 . . 3  class  1
4 caddc 8673 . . 3  class  +
52, 3, 4co 5757 . 2  class  ( 4  +  1 )
61, 5wceq 1619 1  wff  5  =  ( 4  +  1 )
Colors of variables: wff set class
This definition is referenced by:  5re  9754  5pos  9766  4p1e5  9781  3p2e5  9787  4p2e6  9789  5p5e10  9795  5nn  9812  4lt5  9824  6p5e11  10106  7p5e12  10109  8p5e13  10114  8p7e15  10116  9p5e14  10121  9p6e15  10122  5t5e25  10132  6t5e30  10136  7t5e35  10141  8t5e40  10147  9t5e45  10154  ef01bndlem  12391  5prm  13037  lt6abl  15108  log2ublem3  20171  ppiublem2  20369  bclbnd  20446  bposlem6  20455  bposlem9  20458  lgsdir2lem3  20491  rmydioph  26439  expdiophlem2  26447  stoweidlem13  27062
  Copyright terms: Public domain W3C validator