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 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wrdf | |- ( W e. Word V -> W : ( 0 ..^ ( # ` W ) ) --> V ) |
|
2 | 1 | ffvelrnda | |- ( ( W e. Word V /\ I e. ( 0 ..^ ( # ` W ) ) ) -> ( W ` I ) e. V ) |