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

Metamath Proof Explorer

Theorem s2fv0

Description: Extract the first symbol from a doubleton word. (Contributed by Stefan O'Rear, 23-Aug-2015) (Revised by Mario Carneiro, 26-Feb-2016)

Ref Expression
Assertion s2fv0 ⊢ A ∈ V → ⟨“ AB ”⟩ ⁡ 0 = A

Proof

Step Hyp Ref Expression
1 df-s2 ⊢ ⟨“ AB ”⟩ = ⟨“ A ”⟩ ++ ⟨“ B ”⟩
2 s1cli ⊢ ⟨“ A ”⟩ ∈ Word V
3 s1len ⊢ ⟨“ A ”⟩ = 1
4 s1fv ⊢ A ∈ V → ⟨“ A ”⟩ ⁡ 0 = A
5 0nn0 ⊢ 0 ∈ ℕ 0
6 0lt1 ⊢ 0 < 1
7 1 2 3 4 5 6 cats1fv ⊢ A ∈ V → ⟨“ AB ”⟩ ⁡ 0 = A