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

Definition df-splice 11413
Description: Define an operation which replaces portions of words. (Contributed by Stefan O'Rear, 15-Aug-2015.)
Assertion
Ref Expression
df-splice  |- splice  =  ( s  e.  _V , 
b  e.  _V  |->  ( ( ( s substr  <. 0 ,  ( 1st `  ( 1st `  b
) ) >. ) concat  ( 2nd `  b ) ) concat  ( s substr  <. ( 2nd `  ( 1st `  b ) ) ,  ( # `  s
) >. ) ) )
Distinct variable group:    s, b

Detailed syntax breakdown of Definition df-splice
StepHypRef Expression
1 csplice 11407 . 2  class splice
2 vs . . 3  set  s
3 vb . . 3  set  b
4 cvv 2788 . . 3  class  _V
52cv 1622 . . . . . 6  class  s
6 cc0 8737 . . . . . . 7  class  0
73cv 1622 . . . . . . . . 9  class  b
8 c1st 6120 . . . . . . . . 9  class  1st
97, 8cfv 5255 . . . . . . . 8  class  ( 1st `  b )
109, 8cfv 5255 . . . . . . 7  class  ( 1st `  ( 1st `  b
) )
116, 10cop 3643 . . . . . 6  class  <. 0 ,  ( 1st `  ( 1st `  b ) )
>.
12 csubstr 11406 . . . . . 6  class substr
135, 11, 12co 5858 . . . . 5  class  ( s substr  <. 0 ,  ( 1st `  ( 1st `  b
) ) >. )
14 c2nd 6121 . . . . . 6  class  2nd
157, 14cfv 5255 . . . . 5  class  ( 2nd `  b )
16 cconcat 11404 . . . . 5  class concat
1713, 15, 16co 5858 . . . 4  class  ( ( s substr  <. 0 ,  ( 1st `  ( 1st `  b ) ) >.
) concat  ( 2nd `  b
) )
189, 14cfv 5255 . . . . . 6  class  ( 2nd `  ( 1st `  b
) )
19 chash 11337 . . . . . . 7  class  #
205, 19cfv 5255 . . . . . 6  class  ( # `  s )
2118, 20cop 3643 . . . . 5  class  <. ( 2nd `  ( 1st `  b
) ) ,  (
# `  s ) >.
225, 21, 12co 5858 . . . 4  class  ( s substr  <. ( 2nd `  ( 1st `  b ) ) ,  ( # `  s
) >. )
2317, 22, 16co 5858 . . 3  class  ( ( ( s substr  <. 0 ,  ( 1st `  ( 1st `  b ) )
>. ) concat  ( 2nd `  b
) ) concat  ( s substr  <.
( 2nd `  ( 1st `  b ) ) ,  ( # `  s
) >. ) )
242, 3, 4, 4, 23cmpt2 5860 . 2  class  ( s  e.  _V ,  b  e.  _V  |->  ( ( ( s substr  <. 0 ,  ( 1st `  ( 1st `  b ) )
>. ) concat  ( 2nd `  b
) ) concat  ( s substr  <.
( 2nd `  ( 1st `  b ) ) ,  ( # `  s
) >. ) ) )
251, 24wceq 1623 1  wff splice  =  ( s  e.  _V , 
b  e.  _V  |->  ( ( ( s substr  <. 0 ,  ( 1st `  ( 1st `  b
) ) >. ) concat  ( 2nd `  b ) ) concat  ( s substr  <. ( 2nd `  ( 1st `  b ) ) ,  ( # `  s
) >. ) ) )
Colors of variables: wff set class
This definition is referenced by:  splval  11466  splcl  11467
  Copyright terms: Public domain W3C validator