Metamath Proof Explorer


Theorem wrdsymbcl

Description: A symbol within a word over an alphabet belongs to the alphabet. (Contributed by Alexander van der Vekens, 28-Jun-2018)

Ref Expression
Assertion wrdsymbcl WWordVI0..^WWIV

Proof

Step Hyp Ref Expression
1 wrdf WWordVW:0..^WV
2 1 ffvelrnda WWordVI0..^WWIV