Metamath Proof Explorer

Theorem ccatws1ls

Description: The last symbol of the concatenation of a word with a singleton word is the symbol of the singleton word. (Contributed by AV, 29-Sep-2018) (Proof shortened by AV, 14-Oct-2018)

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

Proof

Step Hyp Ref Expression
1 eqidd ⊢ W ∈ Word V ∧ X ∈ V → W = W
2 ccats1val2 ⊢ W ∈ Word V ∧ X ∈ V ∧ W = W → W ++ ⟨“ X ”⟩ ⁡ W = X
3 1 2 mpd3an3 ⊢ W ∈ Word V ∧ X ∈ V → W ++ ⟨“ X ”⟩ ⁡ W = X