Metamath Proof Explorer


Definition df-splice

Description: Define an operation which replaces portions of words. (Contributed by Stefan O'Rear, 15-Aug-2015) (Revised by AV, 14-Oct-2022)

Ref Expression
Assertion df-splice splice=sV,bVsprefix1st1stb++2ndb++ssubstr2nd1stbs

Detailed syntax breakdown

Step Hyp Ref Expression
0 csplice classsplice
1 vs setvars
2 cvv classV
3 vb setvarb
4 1 cv setvars
5 cpfx classprefix
6 c1st class1st
7 3 cv setvarb
8 7 6 cfv class1stb
9 8 6 cfv class1st1stb
10 4 9 5 co classsprefix1st1stb
11 cconcat class++
12 c2nd class2nd
13 7 12 cfv class2ndb
14 10 13 11 co classsprefix1st1stb++2ndb
15 csubstr classsubstr
16 8 12 cfv class2nd1stb
17 chash class.
18 4 17 cfv classs
19 16 18 cop class2nd1stbs
20 4 19 15 co classssubstr2nd1stbs
21 14 20 11 co classsprefix1st1stb++2ndb++ssubstr2nd1stbs
22 1 3 2 2 21 cmpo classsV,bVsprefix1st1stb++2ndb++ssubstr2nd1stbs
23 0 22 wceq wffsplice=sV,bVsprefix1st1stb++2ndb++ssubstr2nd1stbs