Definition df-s8 11294

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 11287	. 2 class <" A B C D E F G H ">
10	1, 2, 3, 4, 5, 6, 7	cs7 11286	. . 3 class <" A B C D E F G ">
11	8	cs1 11148	. . 3 class <" H ">
12		cconcat 11125	. . 3 class ++
13	10, 11, 12	co 6001	. 2 class ( <" A B C D E F G "> ++ <" H "> )
14	9, 13	wceq 1395	1 wff <" A B C D E F G H "> = ( <" A B C D E F G "> ++ <" H "> )

This definition is referenced by:  s8eqd  11308  s8cld  11316