Metamath Proof Explorer

Definition df-s2

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

Ref Expression
Assertion df-s2 
|- <" A B "> = ( <" A "> ++ <" B "> )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cA 
 |-  A
1 cB 
 |-  B
2 0 1 cs2 
 |-  <" A B ">
3 0 cs1 
 |-  <" A ">
4 cconcat 
 |-  ++
5 1 cs1 
 |-  <" B ">
6 3 5 4 co 
 |-  ( <" A "> ++ <" B "> )
7 2 6 wceq 
 |-  <" A B "> = ( <" A "> ++ <" B "> )