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

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

Detailed syntax breakdown of Definition df-splice
StepHypRef Expression
1 csplice 12539 . 2
2 vs . . 3
3 vb . . 3
4 cvv 3109 . . 3
52cv 1394 . . . . . 6
6 cc0 9513 . . . . . . 7
73cv 1394 . . . . . . . . 9
8 c1st 6798 . . . . . . . . 9
97, 8cfv 5593 . . . . . . . 8
109, 8cfv 5593 . . . . . . 7
116, 10cop 4035 . . . . . 6
12 csubstr 12538 . . . . . 6
135, 11, 12co 6296 . . . . 5
14 c2nd 6799 . . . . . 6
157, 14cfv 5593 . . . . 5
16 cconcat 12536 . . . . 5
1713, 15, 16co 6296 . . . 4
189, 14cfv 5593 . . . . . 6
19 chash 12405 . . . . . . 7
205, 19cfv 5593 . . . . . 6
2118, 20cop 4035 . . . . 5
225, 21, 12co 6296 . . . 4
2317, 22, 16co 6296 . . 3
242, 3, 4, 4, 23cmpt2 6298 . 2
251, 24wceq 1395 1
Colors of variables: wff setvar class
This definition is referenced by:  splval  12727  splcl  12728
  Copyright terms: Public domain W3C validator