Definition df-word 12542

Description: Define the class of words over a set. A word is a finite sequence of symbols from a set. The domain is forced so that two words with the same symbols in the same order will be the same. This is sometimes denoted with the Kleene star, although properly speaking that is an operator on languages. (Contributed by FL, 14-Jan-2014.) (Revised by Stefan O'Rear, 14-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.)

Assertion

Ref	Expression
df-word

Distinct variable group:   ,,S

Detailed syntax breakdown of Definition df-word

Step	Hyp	Ref	Expression
1		cS	. . 3
2	1	cword 12534	. 2
3		cc0 9513	. . . . . 6
4		vl	. . . . . . 7
5	4	cv 1394	. . . . . 6
6		cfzo 11824	. . . . . 6
7	3, 5, 6	co 6296	. . . . 5
8		vw	. . . . . 6
9	8	cv 1394	. . . . 5
10	7, 1, 9	wf 5589	. . . 4
11		cn0 10820	. . . 4
12	10, 4, 11	wrex 2808	. . 3
13	12, 8	cab 2442	. 2
14	2, 13	wceq 1395	1

This definition is referenced by:  iswrd  12550  wrdval  12551  nfwrd  12569  csbwrdg  12570