Definition df-s8 12585

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 12578	. 2 class <" A B C D E F G H ">
10	1, 2, 3, 4, 5, 6, 7	cs7 12577	. . 3 class <" A B C D E F G ">
11	8	cs1 12328	. . 3 class <" H ">
12		cconcat 12327	. . 3 class concat
13	10, 11, 12	co 6192	. 2 class ( <" A B C D E F G "> concat <" H "> )
14	9, 13	wceq 1370	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  12599  s8cld  12606  s8cli  12615  s8len  12627  s1s7  12642  s4s4  12646