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 \in Word V \land X \in V) \to W ++ ⟨“ X ”⟩ \in Word V$

Step	Hyp	Ref	Expression
1		s1cl	$⊢ X \in V \to ⟨“ X ”⟩ \in Word V$
2		ccatcl	$⊢ (W \in Word V \land ⟨“ X ”⟩ \in Word V) \to W ++ ⟨“ X ”⟩ \in Word V$
3	1 2	sylan2	$⊢ (W \in Word V \land X \in V) \to W ++ ⟨“ X ”⟩ \in Word V$