Metamath Proof Explorer


Theorem ccatws1clv

Description: The concatenation of a word with a singleton word (which can be over a different alphabet) is a word. (Contributed by AV, 5-Mar-2022)

Ref Expression
Assertion ccatws1clv W Word V W ++ ⟨“ X ”⟩ Word V

Proof

Step Hyp Ref Expression
1 wrdv W Word V W Word V
2 s1cli ⟨“ X ”⟩ Word V
3 ccatcl W Word V ⟨“ X ”⟩ Word V W ++ ⟨“ X ”⟩ Word V
4 1 2 3 sylancl W Word V W ++ ⟨“ X ”⟩ Word V