Definition df-s8 13599

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

Assertion

Ref	Expression
df-s8	|- <" A B C D E F G H "> = ( <" A B C D E F G "> ++ <" H "> )

Detailed syntax breakdown of Definition df-s8

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cB	. . 3 class B
3		cC	. . 3 class C
4		cD	. . 3 class D
5		cE	. . 3 class E
6		cF	. . 3 class F
7		cG	. . 3 class G
8		cH	. . 3 class H
9	1, 2, 3, 4, 5, 6, 7, 8	cs8 13592	. 2 class <" A B C D E F G H ">
10	1, 2, 3, 4, 5, 6, 7	cs7 13591	. . 3 class <" A B C D E F G ">
11	8	cs1 13294	. . 3 class <" H ">
12		cconcat 13293	. . 3 class ++
13	10, 11, 12	co 6650	. 2 class ( <" A B C D E F G "> ++ <" H "> )
14	9, 13	wceq 1483	1 wff <" A B C D E F G H "> = ( <" A B C D E F G "> ++ <" H "> )

This definition is referenced by:  s8eqd  13614  s8cld  13622  s8cli  13631  s8len  13648  s1s7  13673  s4s4  13677