This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem s2cld

Description: A doubleton word is a word. (Contributed by Mario Carneiro, 27-Feb-2016)

Ref Expression
Hypotheses s2cld.1 ⊢ φ → A ∈ X
s2cld.2 ⊢ φ → B ∈ X
Assertion s2cld ⊢ φ → ⟨“ AB ”⟩ ∈ Word X

Proof

Step Hyp Ref Expression
1 s2cld.1 ⊢ φ → A ∈ X
2 s2cld.2 ⊢ φ → B ∈ X
3 df-s2 ⊢ ⟨“ AB ”⟩ = ⟨“ A ”⟩ ++ ⟨“ B ”⟩
4 1 s1cld ⊢ φ → ⟨“ A ”⟩ ∈ Word X
5 3 4 2 cats1cld ⊢ φ → ⟨“ AB ”⟩ ∈ Word X