![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > df-10OLD | Structured version Visualization version GIF version |
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.) |
Ref | Expression |
---|---|
df-10OLD | ⊢ 10 = (9 + 1) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | c10 10955 | . 2 class 10 | |
2 | c9 10954 | . . 3 class 9 | |
3 | c1 9816 | . . 3 class 1 | |
4 | caddc 9818 | . . 3 class + | |
5 | 2, 3, 4 | co 6549 | . 2 class (9 + 1) |
6 | 1, 5 | wceq 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 |