Metamath Proof Explorer

Theorem dp2eq2

Description: Equality theorem for the decimal expansion constructor. (Contributed by David A. Wheeler, 15-May-2015)

Ref Expression
Assertion dp2eq2 
|- ( A = B -> _ C A = _ C B )

Proof

Step Hyp Ref Expression
1 oveq1 
 |-  ( A = B -> ( A / ; 1 0 ) = ( B / ; 1 0 ) )
2 1 oveq2d 
 |-  ( A = B -> ( C + ( A / ; 1 0 ) ) = ( C + ( B / ; 1 0 ) ) )
3 df-dp2 
 |-  _ C A = ( C + ( A / ; 1 0 ) )
4 df-dp2 
 |-  _ C B = ( C + ( B / ; 1 0 ) )
5 2 3 4 3eqtr4g 
 |-  ( A = B -> _ C A = _ C B )