This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ∈ Word V ∧ I ∈ 0 ..^ W → W ⁡ I ∈ V

Proof

Step Hyp Ref Expression
1 wrdf ⊢ W ∈ Word V → W : 0 ..^ W ⟶ V
2 1 ffvelcdmda ⊢ W ∈ Word V ∧ I ∈ 0 ..^ W → W ⁡ I ∈ V