Metamath Proof Explorer

Theorem ccatws1cl

Description: The concatenation of a word with a singleton word is a word. (Contributed by Alexander van der Vekens, 22-Sep-2018)

Ref Expression
Assertion ccatws1cl ⊢ W ∈ Word V ∧ X ∈ V → W ++ ⟨“ X ”⟩ ∈ Word V

Proof

Step Hyp Ref Expression
1 s1cl ⊢ X ∈ V → ⟨“ X ”⟩ ∈ Word V
2 ccatcl ⊢ W ∈ Word V ∧ ⟨“ X ”⟩ ∈ Word V → W ++ ⟨“ X ”⟩ ∈ Word V
3 1 2 sylan2 ⊢ W ∈ Word V ∧ X ∈ V → W ++ ⟨“ X ”⟩ ∈ Word V