df-substr - Metamath Proof Explorer

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

Definition df-substr 12520

Description: Define an operation which extracts portions of words. (Contributed by Stefan O'Rear, 15-Aug-2015.)

**Assertion**
Ref	Expression
df-substr	substr ..^ ..^

**Detailed syntax breakdown of Definition df-substr**
Step	Hyp	Ref	Expression
1		csubstr 12512	. 2 substr
2		vs	. . 3
3		vb	. . 3
4		cvv 3093	. . 3
5		cz 10865	. . . 4
6	5, 5	cxp 4983	. . 3
7	3	cv 1380	. . . . . . 7
8		c1st 6779	. . . . . . 7
9	7, 8	cfv 5574	. . . . . 6
10		c2nd 6780	. . . . . . 7
11	7, 10	cfv 5574	. . . . . 6
12		cfzo 11798	. . . . . 6 ..^
13	9, 11, 12	co 6277	. . . . 5 ..^
14	2	cv 1380	. . . . . 6
15	14	cdm 4985	. . . . 5
16	13, 15	wss 3458	. . . 4 ..^
17		vx	. . . . 5
18		cc0 9490	. . . . . 6
19		cmin 9805	. . . . . . 7
20	11, 9, 19	co 6277	. . . . . 6
21	18, 20, 12	co 6277	. . . . 5 ..^
22	17	cv 1380	. . . . . . 7
23		caddc 9493	. . . . . . 7
24	22, 9, 23	co 6277	. . . . . 6
25	24, 14	cfv 5574	. . . . 5
26	17, 21, 25	cmpt 4491	. . . 4 ..^
27		c0 3767	. . . 4
28	16, 26, 27	cif 3922	. . 3 ..^ ..^
29	2, 3, 4, 6, 28	cmpt2 6279	. 2 ..^ ..^
30	1, 29	wceq 1381	1 substr ..^ ..^

Colors of variables: wff setvar class

This definition is referenced by: swrdval 12618 swrd00 12619 swrdcl 12620 swrd0 12632