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”⟩=\varnothing \mathrm{++}⟨“A”⟩$$

Proof

Step	Hyp	Ref	Expression
1		s1cli	$$⊢⟨“A”⟩\in \mathrm{Word}\mathrm{V}$$
2		ccatlid	$$⊢⟨“A”⟩\in \mathrm{Word}\mathrm{V}\to \varnothing \mathrm{++}⟨“A”⟩=⟨“A”⟩$$
3	1 2	ax-mp	$$⊢\varnothing \mathrm{++}⟨“A”⟩=⟨“A”⟩$$
4	3	eqcomi	$$⊢⟨“A”⟩=\varnothing \mathrm{++}⟨“A”⟩$$