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

Definition df-s6 12938
Description: Define the length 6 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016.)
Assertion
Ref Expression
df-s6  |-  <" A B C D E F ">  =  (
<" A B C D E "> ++  <" F "> )

Detailed syntax breakdown of Definition df-s6
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
71, 2, 3, 4, 5, 6cs6 12931 . 2  class  <" A B C D E F ">
81, 2, 3, 4, 5cs5 12930 . . 3  class  <" A B C D E ">
96cs1 12651 . . 3  class  <" F ">
10 cconcat 12650 . . 3  class ++
118, 9, 10co 6301 . 2  class  ( <" A B C D E "> ++  <" F "> )
127, 11wceq 1437 1  wff  <" A B C D E F ">  =  (
<" A B C D E "> ++  <" F "> )
Colors of variables: wff setvar class
This definition is referenced by:  s6eqd  12952  s6cld  12959  s6cli  12968  s6len  12984  s1s5  12999  s1s6  13000  s4s2  13003  konigsberg  25700
  Copyright terms: Public domain W3C validator