Metamath Proof Explorer

Theorem s2cl

Description: A doubleton word is a word. (Contributed by Stefan O'Rear, 23-Aug-2015) (Revised by Mario Carneiro, 26-Feb-2016)

Ref Expression
Assertion s2cl 
|- ( ( A e. X /\ B e. X ) -> <" A B "> e. Word X )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( A e. X /\ B e. X ) -> A e. X )
2 simpr 
 |-  ( ( A e. X /\ B e. X ) -> B e. X )
3 1 2 s2cld 
 |-  ( ( A e. X /\ B e. X ) -> <" A B "> e. Word X )