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