Definition df-s6

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

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

Detailed syntax breakdown

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