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

Proof

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