Description: A singleton word is a word. (Contributed by Stefan O'Rear, 15-Aug-2015) (Revised by Mario Carneiro, 26-Feb-2016) (Proof shortened by AV, 23-Nov-2018)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | s1cl | |- ( A e. B -> <" A "> e. Word B ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | s1val | |- ( A e. B -> <" A "> = { <. 0 , A >. } ) |
|
| 2 | snopiswrd | |- ( A e. B -> { <. 0 , A >. } e. Word B ) |
|
| 3 | 1 2 | eqeltrd | |- ( A e. B -> <" A "> e. Word B ) |