Metamath Proof Explorer


Theorem cats1cld

Description: Closure of concatenation with a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016)

Ref Expression
Hypotheses cats1cld.1 T = S ++ ⟨“ X ”⟩
cats1cld.2 φ S Word A
cats1cld.3 φ X A
Assertion cats1cld φ T Word A

Proof

Step Hyp Ref Expression
1 cats1cld.1 T = S ++ ⟨“ X ”⟩
2 cats1cld.2 φ S Word A
3 cats1cld.3 φ X A
4 3 s1cld φ ⟨“ X ”⟩ Word A
5 ccatcl S Word A ⟨“ X ”⟩ Word A S ++ ⟨“ X ”⟩ Word A
6 2 4 5 syl2anc φ S ++ ⟨“ X ”⟩ Word A
7 1 6 eqeltrid φ T Word A