Metamath Proof Explorer

Theorem s1cli

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

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

Proof

Step Hyp Ref Expression
1 ids1 
 |-  <" A "> = <" ( _I ` A ) ">
2 fvex 
 |-  ( _I ` A ) e. _V
3 s1cl 
 |-  ( ( _I ` A ) e. _V -> <" ( _I ` A ) "> e. Word _V )
4 2 3 ax-mp 
 |-  <" ( _I ` A ) "> e. Word _V
5 1 4 eqeltri 
 |-  <" A "> e. Word _V