Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-splice Structured version   Visualization version   Unicode version

Definition df-splice 12716
 Description: Define an operation which replaces portions of words. (Contributed by Stefan O'Rear, 15-Aug-2015.)
Assertion
Ref Expression
df-splice splice substr ++ ++ substr
Distinct variable group:   ,

Detailed syntax breakdown of Definition df-splice
StepHypRef Expression
1 csplice 12708 . 2 splice
2 vs . . 3
3 vb . . 3
4 cvv 3031 . . 3
52cv 1451 . . . . . 6
6 cc0 9557 . . . . . . 7
73cv 1451 . . . . . . . . 9
8 c1st 6810 . . . . . . . . 9
97, 8cfv 5589 . . . . . . . 8
109, 8cfv 5589 . . . . . . 7
116, 10cop 3965 . . . . . 6
12 csubstr 12707 . . . . . 6 substr
135, 11, 12co 6308 . . . . 5 substr
14 c2nd 6811 . . . . . 6
157, 14cfv 5589 . . . . 5
16 cconcat 12705 . . . . 5 ++
1713, 15, 16co 6308 . . . 4 substr ++
189, 14cfv 5589 . . . . . 6
19 chash 12553 . . . . . . 7
205, 19cfv 5589 . . . . . 6
2118, 20cop 3965 . . . . 5
225, 21, 12co 6308 . . . 4 substr
2317, 22, 16co 6308 . . 3 substr ++ ++ substr
242, 3, 4, 4, 23cmpt2 6310 . 2 substr ++ ++ substr
251, 24wceq 1452 1 splice substr ++ ++ substr
 Colors of variables: wff setvar class This definition is referenced by:  splval  12912  splcl  12913
 Copyright terms: Public domain W3C validator