Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  splval Structured version   Unicode version

Theorem splval 11781
 Description: Value of the substring replacement operator. (Contributed by Stefan O'Rear, 15-Aug-2015.)
Assertion
Ref Expression
splval splice substr concat concat substr

Proof of Theorem splval
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-splice 11728 . . 3 splice substr concat concat substr
21a1i 11 . 2 splice substr concat concat substr
3 simprl 734 . . . . 5
4 fveq2 5729 . . . . . . . . 9
54fveq2d 5733 . . . . . . . 8
65adantl 454 . . . . . . 7
7 ot1stg 6362 . . . . . . . 8
87adantl 454 . . . . . . 7
96, 8sylan9eqr 2491 . . . . . 6
109opeq2d 3992 . . . . 5
113, 10oveq12d 6100 . . . 4 substr substr
12 fveq2 5729 . . . . . 6
1312adantl 454 . . . . 5
14 ot3rdg 6364 . . . . . . 7
15143ad2ant3 981 . . . . . 6
1615adantl 454 . . . . 5
1713, 16sylan9eqr 2491 . . . 4
1811, 17oveq12d 6100 . . 3 substr concat substr concat
194fveq2d 5733 . . . . . . 7
2019adantl 454 . . . . . 6
21 ot2ndg 6363 . . . . . . 7
2221adantl 454 . . . . . 6
2320, 22sylan9eqr 2491 . . . . 5
243fveq2d 5733 . . . . 5
2523, 24opeq12d 3993 . . . 4
263, 25oveq12d 6100 . . 3 substr substr
2718, 26oveq12d 6100 . 2 substr concat concat substr substr concat concat substr
28 elex 2965 . . 3