Theorem ccatw2s1ccatws2

Description: The concatenation of a word with two singleton words equals the concatenation of the word with the doubleton word consisting of the symbols of the two singletons. (Contributed by Mario Carneiro/AV, 21-Oct-2018) (Revised by AV, 29-Jan-2024)

	Ref	Expression
Assertion	ccatw2s1ccatws2	|- ( W e. Word V -> ( ( W ++ <" X "> ) ++ <" Y "> ) = ( W ++ <" X Y "> ) )

Proof

Step	Hyp	Ref	Expression
1		ccatw2s1ass	|- ( W e. Word V -> ( ( W ++ <" X "> ) ++ <" Y "> ) = ( W ++ ( <" X "> ++ <" Y "> ) ) )
2		df-s2	|- <" X Y "> = ( <" X "> ++ <" Y "> )
3	2	eqcomi	|- ( <" X "> ++ <" Y "> ) = <" X Y ">
4	3	a1i	|- ( W e. Word V -> ( <" X "> ++ <" Y "> ) = <" X Y "> )
5	4	oveq2d	|- ( W e. Word V -> ( W ++ ( <" X "> ++ <" Y "> ) ) = ( W ++ <" X Y "> ) )
6	1 5	eqtrd	|- ( W e. Word V -> ( ( W ++ <" X "> ) ++ <" Y "> ) = ( W ++ <" X Y "> ) )