Description: A singleton word is not the empty string. (Contributed by Mario Carneiro, 27-Feb-2016) (Proof shortened by Kyle Wyonch, 18-Jul-2021)
Ref | Expression | ||
---|---|---|---|
Assertion | s1nz | |- <" A "> =/= (/) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-s1 | |- <" A "> = { <. 0 , ( _I ` A ) >. } |
|
2 | opex | |- <. 0 , ( _I ` A ) >. e. _V |
|
3 | 2 | snnz | |- { <. 0 , ( _I ` A ) >. } =/= (/) |
4 | 1 3 | eqnetri | |- <" A "> =/= (/) |