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

Metamath Proof Explorer

Theorem fstwrdne

Description: The first symbol of a nonempty word is an element of the alphabet for the word. (Contributed by AV, 28-Sep-2018) (Proof shortened by AV, 14-Oct-2018)

Ref Expression
Assertion fstwrdne ⊢ W ∈ Word V ∧ W ≠ ∅ → W ⁡ 0 ∈ V

Proof

Step Hyp Ref Expression
1 wrdlenge1n0 ⊢ W ∈ Word V → W ≠ ∅ ↔ 1 ≤ W
2 wrdsymb1 ⊢ W ∈ Word V ∧ 1 ≤ W → W ⁡ 0 ∈ V
3 2 ex ⊢ W ∈ Word V → 1 ≤ W → W ⁡ 0 ∈ V
4 1 3 sylbid ⊢ W ∈ Word V → W ≠ ∅ → W ⁡ 0 ∈ V
5 4 imp ⊢ W ∈ Word V ∧ W ≠ ∅ → W ⁡ 0 ∈ V