Metamath Proof Explorer
Description: A decimal number is a set. (Contributed by Mario Carneiro, 17-Apr-2015)
(Revised by AV, 6-Sep-2021)
|
|
Ref |
Expression |
|
Assertion |
decex |
Could not format assertion : No typesetting found for |- ; A B e. _V with typecode |- |
Proof
| Step |
Hyp |
Ref |
Expression |
| 1 |
|
df-dec |
Could not format ; A B = ( ( ( 9 + 1 ) x. A ) + B ) : No typesetting found for |- ; A B = ( ( ( 9 + 1 ) x. A ) + B ) with typecode |- |
| 2 |
1
|
ovexi |
Could not format ; A B e. _V : No typesetting found for |- ; A B e. _V with typecode |- |