Metamath Proof Explorer

Theorem decex

Description: A decimal number is a set. (Contributed by Mario Carneiro, 17-Apr-2015) (Revised by AV, 6-Sep-2021)

Ref Expression
Assertion decex 
|- ; A B e. _V

Proof

Step Hyp Ref Expression
1 df-dec 
 |-  ; A B = ( ( ( 9 + 1 ) x. A ) + B )
2 1 ovexi 
 |-  ; A B e. _V