This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 𝐴 𝐵 ∈ V

Proof

Step Hyp Ref Expression
1 df-dec ⊢ 𝐴 𝐵 = ( ( ( 9 + 1 ) · 𝐴 ) + 𝐵 )
2 1 ovexi ⊢ 𝐴 𝐵 ∈ V