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 
|- ( ( W e. Word V /\ I e. ( 0 ..^ ( # ` W ) ) ) -> ( W ` I ) e. V )

Proof

Step Hyp Ref Expression
1 wrdf 
 |-  ( W e. Word V -> W : ( 0 ..^ ( # ` W ) ) --> V )
2 1 ffvelcdmda 
 |-  ( ( W e. Word V /\ I e. ( 0 ..^ ( # ` W ) ) ) -> ( W ` I ) e. V )