Metamath Proof Explorer


Theorem s0s1

Description: Concatenation of fixed length strings. (This special case of ccatlid is provided to complete the pattern s0s1 , df-s2 , df-s3 , ...) (Contributed by Mario Carneiro, 28-Feb-2016)

Ref Expression
Assertion s0s1
|- <" A "> = ( (/) ++ <" A "> )

Proof

Step Hyp Ref Expression
1 s1cli
 |-  <" A "> e. Word _V
2 ccatlid
 |-  ( <" A "> e. Word _V -> ( (/) ++ <" A "> ) = <" A "> )
3 1 2 ax-mp
 |-  ( (/) ++ <" A "> ) = <" A ">
4 3 eqcomi
 |-  <" A "> = ( (/) ++ <" A "> )