Definition df-s2

Description: Define the length 2 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016)

	Ref	Expression
Assertion	df-s2	⊢ ⟨“ 𝐴 𝐵 ”⟩ = ( ⟨“ 𝐴 ”⟩ ++ ⟨“ 𝐵 ”⟩ )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	⊢ 𝐴
1		cB	⊢ 𝐵
2	0 1	cs2	⊢ ⟨“ 𝐴 𝐵 ”⟩
3	0	cs1	⊢ ⟨“ 𝐴 ”⟩
4		cconcat	⊢ ++
5	1	cs1	⊢ ⟨“ 𝐵 ”⟩
6	3 5 4	co	⊢ ( ⟨“ 𝐴 ”⟩ ++ ⟨“ 𝐵 ”⟩ )
7	2 6	wceq	⊢ ⟨“ 𝐴 𝐵 ”⟩ = ( ⟨“ 𝐴 ”⟩ ++ ⟨“ 𝐵 ”⟩ )