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 12225

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 12217	. 2 substr
2		vs	. . 3
3		vb	. . 3
4		cvv 2967	. . 3
5		cz 10638	. . . 4
6	5, 5	cxp 4833	. . 3
7	3	cv 1368	. . . . . . 7
8		c1st 6570	. . . . . . 7
9	7, 8	cfv 5413	. . . . . 6
10		c2nd 6571	. . . . . . 7
11	7, 10	cfv 5413	. . . . . 6
12		cfzo 11540	. . . . . 6 ..^
13	9, 11, 12	co 6086	. . . . 5 ..^
14	2	cv 1368	. . . . . 6
15	14	cdm 4835	. . . . 5
16	13, 15	wss 3323	. . . 4 ..^
17		vx	. . . . 5
18		cc0 9274	. . . . . 6
19		cmin 9587	. . . . . . 7
20	11, 9, 19	co 6086	. . . . . 6
21	18, 20, 12	co 6086	. . . . 5 ..^
22	17	cv 1368	. . . . . . 7
23		caddc 9277	. . . . . . 7
24	22, 9, 23	co 6086	. . . . . 6
25	24, 14	cfv 5413	. . . . 5
26	17, 21, 25	cmpt 4345	. . . 4 ..^
27		c0 3632	. . . 4
28	16, 26, 27	cif 3786	. . 3 ..^ ..^
29	2, 3, 4, 6, 28	cmpt2 6088	. 2 ..^ ..^
30	1, 29	wceq 1369	1 substr ..^ ..^

Colors of variables: wff setvar class

This definition is referenced by: swrdval 12305 swrd00 12306 swrdcl 12307 swrd0 12319