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

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

Detailed syntax breakdown of Definition df-splice
StepHypRef Expression
1 csplice 11726 . 2 splice
2 vs . . 3
3 vb . . 3
4 cvv 2958 . . 3
52cv 1652 . . . . . 6
6 cc0 8995 . . . . . . 7
73cv 1652 . . . . . . . . 9
8 c1st 6350 . . . . . . . . 9
97, 8cfv 5457 . . . . . . . 8
109, 8cfv 5457 . . . . . . 7
116, 10cop 3819 . . . . . 6
12 csubstr 11725 . . . . . 6 substr
135, 11, 12co 6084 . . . . 5 substr
14 c2nd 6351 . . . . . 6
157, 14cfv 5457 . . . . 5
16 cconcat 11723 . . . . 5 concat
1713, 15, 16co 6084 . . . 4 substr concat
189, 14cfv 5457 . . . . . 6
19 chash 11623 . . . . . . 7
205, 19cfv 5457 . . . . . 6
2118, 20cop 3819 . . . . 5
225, 21, 12co 6084 . . . 4 substr
2317, 22, 16co 6084 . . 3 substr concat concat substr
242, 3, 4, 4, 23cmpt2 6086 . 2 substr concat concat substr
251, 24wceq 1653 1 splice substr concat concat substr
 Colors of variables: wff set class This definition is referenced by:  splval  11785  splcl  11786
 Copyright terms: Public domain W3C validator