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

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

Detailed syntax breakdown of Definition df-s5
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
61, 2, 3, 4, 5cs5 12800 . 2  class  <" A B C D E ">
71, 2, 3, 4cs4 12799 . . 3  class  <" A B C D ">
85cs1 12521 . . 3  class  <" E ">
9 cconcat 12520 . . 3  class ++
107, 8, 9co 6270 . 2  class  ( <" A B C D "> ++  <" E "> )
116, 10wceq 1398 1  wff  <" A B C D E ">  =  ( <" A B C D "> ++  <" E "> )
Colors of variables: wff setvar class
This definition is referenced by:  s5eqd  12821  s5cld  12828  s5cli  12837  s5len  12849  s1s4  12864  s1s5  12865  s4s2  12869  konigsberg  25189
  Copyright terms: Public domain W3C validator