Description: Extract the last symbol of a word. May be not meaningful for other sets which are not words. (Contributed by Alexander van der Vekens, 18-Mar-2018)
Ref | Expression | ||
---|---|---|---|
Assertion | lsw | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elex | |
|
2 | fvex | |
|
3 | id | |
|
4 | fveq2 | |
|
5 | 4 | oveq1d | |
6 | 3 5 | fveq12d | |
7 | df-lsw | |
|
8 | 6 7 | fvmptg | |
9 | 1 2 8 | sylancl | |