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	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 ‘ 𝐼 ) ∈ 𝑉 )

Proof

Step	Hyp	Ref	Expression
1		wrdf	⊢ ( 𝑊 ∈ Word 𝑉 → 𝑊 : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝑉 )
2	1	ffvelcdmda	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 ‘ 𝐼 ) ∈ 𝑉 )