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

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
StepHypRef Expression
1 cS . . 3
21cword 12534 . 2
3 cc0 9513 . . . . . 6
4 vl . . . . . . 7
54cv 1394 . . . . . 6
6 cfzo 11824 . . . . . 6
73, 5, 6co 6296 . . . . 5
8 vw . . . . . 6
98cv 1394 . . . . 5
107, 1, 9wf 5589 . . . 4
11 cn0 10820 . . . 4
1210, 4, 11wrex 2808 . . 3
1312, 8cab 2442 . 2
142, 13wceq 1395 1
Colors of variables: wff setvar class
This definition is referenced by:  iswrd  12550  wrdval  12551  nfwrd  12569  csbwrdg  12570
  Copyright terms: Public domain W3C validator