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 10964
Description: Define the number 10. See remarks under df-2 10956. (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 10955 . 2 class 10
2 c9 10954 . . 3 class 9
3 c1 9816 . . 3 class 1
4 caddc 9818 . . 3 class +
52, 3, 4co 6549 . 2 class (9 + 1)
61, 5wceq 1475 1 wff 10 = (9 + 1)
Colors of variables: wff setvar class
This definition is referenced by:  10reOLD  10986  10posOLD  11000  9p1e10OLD  11036  5p5e10OLD  11045  6p4e10OLD  11048  7p3e10OLD  11050  8p2e10OLD  11051  10nnOLD  11070  9lt10OLD  11107  decsuccOLD  11427  9p2e11OLD  11496  0.999...OLD  14452  3dvdsOLD  14891  3dvdsdecOLD  14893  3dvds2decOLD  14895
  Copyright terms: Public domain W3C validator