Definition df-s2

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

	Ref	Expression
Assertion	df-s2	$$⊢⟨“AB”⟩=⟨“A”⟩\mathrm{++}⟨“B”⟩$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	$$classA$$
1		cB	$$classB$$
2	0 1	cs2	$$class⟨“AB”⟩$$
3	0	cs1	$$class⟨“A”⟩$$
4		cconcat	$$class\mathrm{++}$$
5	1	cs1	$$class⟨“B”⟩$$
6	3 5 4	co	$$class\left(⟨“A”⟩\mathrm{++}⟨“B”⟩\right)$$
7	2 6	wceq	$$wff⟨“AB”⟩=⟨“A”⟩\mathrm{++}⟨“B”⟩$$