Definition df-s5

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

	Ref	Expression
Assertion	df-s5	$$⊢⟨“ABCDE”⟩=⟨“ABCD”⟩\mathrm{++}⟨“E”⟩$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	$$classA$$
1		cB	$$classB$$
2		cC	$$classC$$
3		cD	$$classD$$
4		cE	$$classE$$
5	0 1 2 3 4	cs5	$$class⟨“ABCDE”⟩$$
6	0 1 2 3	cs4	$$class⟨“ABCD”⟩$$
7		cconcat	$$class\mathrm{++}$$
8	4	cs1	$$class⟨“E”⟩$$
9	6 8 7	co	$$class\left(⟨“ABCD”⟩\mathrm{++}⟨“E”⟩\right)$$
10	5 9	wceq	$$wff⟨“ABCDE”⟩=⟨“ABCD”⟩\mathrm{++}⟨“E”⟩$$