Definition df-s5

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

	Ref	Expression
Assertion	df-s5	⊢ ⟨“ 𝐴 𝐵 𝐶 𝐷 𝐸 ”⟩ = ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ++ ⟨“ 𝐸 ”⟩ )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	⊢ 𝐴
1		cB	⊢ 𝐵
2		cC	⊢ 𝐶
3		cD	⊢ 𝐷
4		cE	⊢ 𝐸
5	0 1 2 3 4	cs5	⊢ ⟨“ 𝐴 𝐵 𝐶 𝐷 𝐸 ”⟩
6	0 1 2 3	cs4	⊢ ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩
7		cconcat	⊢ ++
8	4	cs1	⊢ ⟨“ 𝐸 ”⟩
9	6 8 7	co	⊢ ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ++ ⟨“ 𝐸 ”⟩ )
10	5 9	wceq	⊢ ⟨“ 𝐴 𝐵 𝐶 𝐷 𝐸 ”⟩ = ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ++ ⟨“ 𝐸 ”⟩ )