Metamath Proof Explorer

Theorem s1cld

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

Ref Expression
Hypothesis s1cld.1 
|- ( ph -> A e. B )
Assertion s1cld 
|- ( ph -> <" A "> e. Word B )

Proof

Step Hyp Ref Expression
1 s1cld.1 
 |-  ( ph -> A e. B )
2 s1cl 
 |-  ( A e. B -> <" A "> e. Word B )
3 1 2 syl 
 |-  ( ph -> <" A "> e. Word B )