Metamath Proof Explorer

Theorem fzssz

Description: A finite sequence of integers is a set of integers. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Assertion fzssz 
|- ( M ... N ) C_ ZZ

Proof

Step Hyp Ref Expression
1 elfzelz 
 |-  ( x e. ( M ... N ) -> x e. ZZ )
2 1 ssriv 
 |-  ( M ... N ) C_ ZZ