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

Definition df-s7 12780
Description: Define the length 7 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016.)
Assertion
Ref Expression
df-s7  |-  <" A B C D E F G ">  =  ( <" A B C D E F "> concat  <" G "> )

Detailed syntax breakdown of Definition df-s7
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
81, 2, 3, 4, 5, 6, 7cs7 12773 . 2  class  <" A B C D E F G ">
91, 2, 3, 4, 5, 6cs6 12772 . . 3  class  <" A B C D E F ">
107cs1 12502 . . 3  class  <" G ">
11 cconcat 12501 . . 3  class concat
129, 10, 11co 6283 . 2  class  ( <" A B C D E F "> concat 
<" G "> )
138, 12wceq 1379 1  wff  <" A B C D E F G ">  =  ( <" A B C D E F "> concat  <" G "> )
Colors of variables: wff setvar class
This definition is referenced by:  s7eqd  12794  s7cld  12801  s7cli  12810  s7len  12822  s1s6  12837  s1s7  12838  s4s3  12841  konigsberg  24679
  Copyright terms: Public domain W3C validator