Metamath Proof Explorer

Theorem wrd0

Description: The empty set is a word (theempty word, frequently denoted ε in this context). This corresponds to the definition in Section 9.1 of AhoHopUll p. 318. (Contributed by Stefan O'Rear, 15-Aug-2015) (Proof shortened by AV, 13-May-2020)

Ref Expression
Assertion wrd0 
|- (/) e. Word S

Proof

Step Hyp Ref Expression
1 f0 
 |-  (/) : (/) --> S
2 iswrddm0 
 |-  ( (/) : (/) --> S -> (/) e. Word S )
3 1 2 ax-mp 
 |-  (/) e. Word S