Metamath Proof Explorer

Definition df-s5

Description: Define the length 5 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016)

Ref Expression
Assertion df-s5 
|- <" A B C D E "> = ( <" A B C D "> ++ <" E "> )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cA 
 |-  A
1 cB 
 |-  B
2 cC 
 |-  C
3 cD 
 |-  D
4 cE 
 |-  E
5 0 1 2 3 4 cs5 
 |-  <" A B C D E ">
6 0 1 2 3 cs4 
 |-  <" A B C D ">
7 cconcat 
 |-  ++
8 4 cs1 
 |-  <" E ">
9 6 8 7 co 
 |-  ( <" A B C D "> ++ <" E "> )
10 5 9 wceq 
 |-  <" A B C D E "> = ( <" A B C D "> ++ <" E "> )