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