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

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

Detailed syntax breakdown of Definition df-substr
StepHypRef Expression
1 csubstr 11720 . 2 substr
2 vs . . 3
3 vb . . 3
4 cvv 2956 . . 3
5 cz 10282 . . . 4
65, 5cxp 4876 . . 3
73cv 1651 . . . . . . 7
8 c1st 6347 . . . . . . 7
97, 8cfv 5454 . . . . . 6
10 c2nd 6348 . . . . . . 7
117, 10cfv 5454 . . . . . 6
12 cfzo 11135 . . . . . 6 ..^
139, 11, 12co 6081 . . . . 5 ..^
142cv 1651 . . . . . 6
1514cdm 4878 . . . . 5
1613, 15wss 3320 . . . 4 ..^
17 vx . . . . 5
18 cc0 8990 . . . . . 6
19 cmin 9291 . . . . . . 7
2011, 9, 19co 6081 . . . . . 6
2118, 20, 12co 6081 . . . . 5 ..^
2217cv 1651 . . . . . . 7
23 caddc 8993 . . . . . . 7
2422, 9, 23co 6081 . . . . . 6
2524, 14cfv 5454 . . . . 5
2617, 21, 25cmpt 4266 . . . 4 ..^
27 c0 3628 . . . 4
2816, 26, 27cif 3739 . . 3 ..^ ..^
292, 3, 4, 6, 28cmpt2 6083 . 2 ..^ ..^
301, 29wceq 1652 1 substr ..^ ..^
 Colors of variables: wff set class This definition is referenced by:  swrdval  11764  swrd00  11765  swrdcl  11766
 Copyright terms: Public domain W3C validator