Definition df-s8 12769

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 "> concat <" 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 12762	. 2 class <" A B C D E F G H ">
10	1, 2, 3, 4, 5, 6, 7	cs7 12761	. . 3 class <" A B C D E F G ">
11	8	cs1 12490	. . 3 class <" H ">
12		cconcat 12489	. . 3 class concat
13	10, 11, 12	co 6275	. 2 class ( <" A B C D E F G "> concat <" H "> )
14	9, 13	wceq 1374	1 wff <" A B C D E F G H "> = ( <" A B C D E F G "> concat <" H "> )

This definition is referenced by:  s8eqd  12783  s8cld  12790  s8cli  12799  s8len  12811  s1s7  12826  s4s4  12830