Metamath Proof Explorer

Theorem s2cli

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

Ref Expression
Assertion s2cli 
|- <" A B "> e. Word _V

Proof

Step Hyp Ref Expression
1 df-s2 
 |-  <" A B "> = ( <" A "> ++ <" B "> )
2 s1cli 
 |-  <" A "> e. Word _V
3 1 2 cats1cli 
 |-  <" A B "> e. Word _V