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

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

Detailed syntax breakdown of Definition df-substr
StepHypRef Expression
1 csubstr 12538 . 2
2 vs . . 3
3 vb . . 3
4 cvv 3109 . . 3
5 cz 10889 . . . 4
65, 5cxp 5002 . . 3
73cv 1394 . . . . . . 7
8 c1st 6798 . . . . . . 7
97, 8cfv 5593 . . . . . 6
10 c2nd 6799 . . . . . . 7
117, 10cfv 5593 . . . . . 6
12 cfzo 11824 . . . . . 6
139, 11, 12co 6296 . . . . 5
142cv 1394 . . . . . 6
1514cdm 5004 . . . . 5
1613, 15wss 3475 . . . 4
17 vx . . . . 5
18 cc0 9513 . . . . . 6
19 cmin 9828 . . . . . . 7
2011, 9, 19co 6296 . . . . . 6
2118, 20, 12co 6296 . . . . 5
2217cv 1394 . . . . . . 7
23 caddc 9516 . . . . . . 7
2422, 9, 23co 6296 . . . . . 6
2524, 14cfv 5593 . . . . 5
2617, 21, 25cmpt 4510 . . . 4
27 c0 3784 . . . 4
2816, 26, 27cif 3941 . . 3
292, 3, 4, 6, 28cmpt2 6298 . 2
301, 29wceq 1395 1
Colors of variables: wff setvar class
This definition is referenced by:  swrdval  12644  swrd00  12645  swrdcl  12646  swrd0  12658
  Copyright terms: Public domain W3C validator