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 ⟨“ 𝐴 ”⟩ = ( ∅ ++ ⟨“ 𝐴 ”⟩ )

Proof

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