MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-s8 Structured version   Unicode version

Definition df-s8 12798
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
StepHypRef 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
91, 2, 3, 4, 5, 6, 7, 8cs8 12791 . 2  class  <" A B C D E F G H ">
101, 2, 3, 4, 5, 6, 7cs7 12790 . . 3  class  <" A B C D E F G ">
118cs1 12516 . . 3  class  <" H ">
12 cconcat 12515 . . 3  class concat
1310, 11, 12co 6281 . 2  class  ( <" A B C D E F G "> concat  <" H "> )
149, 13wceq 1383 1  wff  <" A B C D E F G H ">  =  ( <" A B C D E F G "> concat  <" H "> )
Colors of variables: wff setvar class
This definition is referenced by:  s8eqd  12812  s8cld  12819  s8cli  12828  s8len  12840  s1s7  12855  s4s4  12859
  Copyright terms: Public domain W3C validator