Definition df-pfx 11164

Description: Define an operation which extracts prefixes of words, i.e. subwords (or substrings) starting at the beginning of a word (or string). In other words, ( S prefix L ) is the prefix of the word S of length L. Definition in Section 9.1 of [AhoHopUll] p. 318. See also Wikipedia "Substring" https://en.wikipedia.org/wiki/Substring#Prefix. (Contributed by AV, 2-May-2020.)

Assertion

Ref	Expression
df-pfx	|- prefix = ( s e. _V , l e. NN0 |-> ( s substr <. 0 , l >. ) )

Distinct variable group:   s, l

Detailed syntax breakdown of Definition df-pfx

Step	Hyp	Ref	Expression
1		cpfx 11163	. 2 class prefix
2		vs	. . 3 setvar s
3		vl	. . 3 setvar l
4		cvv 2776	. . 3 class _V
5		cn0 9330	. . 3 class NN0
6	2	cv 1372	. . . 4 class s
7		cc0 7960	. . . . 5 class 0
8	3	cv 1372	. . . . 5 class l
9	7, 8	cop 3646	. . . 4 class <. 0 , l >.
10		csubstr 11136	. . . 4 class substr
11	6, 9, 10	co 5967	. . 3 class ( s substr <. 0 , l >. )
12	2, 3, 4, 5, 11	cmpo 5969	. 2 class ( s e. _V , l e. NN0 |-> ( s substr <. 0 , l >. ) )
13	1, 12	wceq 1373	1 wff prefix = ( s e. _V , l e. NN0 |-> ( s substr <. 0 , l >. ) )

This definition is referenced by:  pfxval  11165  fnpfx  11168