Description: Membership in a set of sequential integers with an appended element. (Contributed by NM, 7-Dec-2005) (Revised by Mario Carneiro, 28-Apr-2015)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | fzelp1 | |- ( K e. ( M ... N ) -> K e. ( M ... ( N + 1 ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | fzssp1 | |- ( M ... N ) C_ ( M ... ( N + 1 ) ) |
|
| 2 | 1 | sseli | |- ( K e. ( M ... N ) -> K e. ( M ... ( N + 1 ) ) ) |