MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-10OLD Structured version   Visualization version   GIF version

Definition df-10OLD 11300
Description: Define the number 10. See remarks under df-2 11292. (Contributed by NM, 5-Feb-2007.) Obsolete as of 9-Sep-2021. (New usage is discouraged.)
Assertion
Ref Expression
df-10OLD 10 = (9 + 1)

Detailed syntax breakdown of Definition df-10OLD
StepHypRef Expression
1 c10 11291 . 2 class 10
2 c9 11290 . . 3 class 9
3 c1 10150 . . 3 class 1
4 caddc 10152 . . 3 class +
52, 3, 4co 6815 . 2 class (9 + 1)
61, 5wceq 1632 1 wff 10 = (9 + 1)
Colors of variables: wff setvar class
This definition is referenced by:  10reOLD  11322  10posOLD  11336  9p1e10OLD  11372  5p5e10OLD  11381  6p4e10OLD  11384  7p3e10OLD  11386  8p2e10OLD  11387  10nnOLD  11406  9lt10OLD  11443  decsuccOLD  11764  9p2e11OLD  11833  0.999...OLD  14833  3dvdsOLD  15276  3dvdsdecOLD  15278  3dvds2decOLD  15280
  Copyright terms: Public domain W3C validator