Definition df-s8 12941

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 12934	. 2 class <" A B C D E F G H ">
10	1, 2, 3, 4, 5, 6, 7	cs7 12933	. . 3 class <" A B C D E F G ">
11	8	cs1 12652	. . 3 class <" H ">
12		cconcat 12651	. . 3 class ++
13	10, 11, 12	co 6302	. 2 class ( <" A B C D E F G "> ++ <" H "> )
14	9, 13	wceq 1437	1 wff <" A B C D E F G H "> = ( <" A B C D E F G "> ++ <" H "> )

This definition is referenced by:  s8eqd  12955  s8cld  12962  s8cli  12971  s8len  12987  s1s7  13002  s4s4  13006