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

Metamath Proof Explorer

Theorem s0s1

Description: Concatenation of fixed length strings. (This special case of ccatlid is provided to complete the pattern s0s1 , df-s2 , df-s3 , ...) (Contributed by Mario Carneiro, 28-Feb-2016)

Ref Expression
Assertion s0s1 ⊢ ⟨“ A ”⟩ = ∅ ++ ⟨“ A ”⟩

Proof

Step Hyp Ref Expression
1 s1cli ⊢ ⟨“ A ”⟩ ∈ Word V
2 ccatlid ⊢ ⟨“ A ”⟩ ∈ Word V → ∅ ++ ⟨“ A ”⟩ = ⟨“ A ”⟩
3 1 2 ax-mp ⊢ ∅ ++ ⟨“ A ”⟩ = ⟨“ A ”⟩
4 3 eqcomi ⊢ ⟨“ A ”⟩ = ∅ ++ ⟨“ A ”⟩