Metamath Proof Explorer


Theorem fzsn

Description: A finite interval of integers with one element. (Contributed by Jeff Madsen, 2-Sep-2009)

Ref Expression
Assertion fzsn
|- ( M e. ZZ -> ( M ... M ) = { M } )

Proof

Step Hyp Ref Expression
1 elfz1eq
 |-  ( k e. ( M ... M ) -> k = M )
2 elfz3
 |-  ( M e. ZZ -> M e. ( M ... M ) )
3 eleq1
 |-  ( k = M -> ( k e. ( M ... M ) <-> M e. ( M ... M ) ) )
4 2 3 syl5ibrcom
 |-  ( M e. ZZ -> ( k = M -> k e. ( M ... M ) ) )
5 1 4 impbid2
 |-  ( M e. ZZ -> ( k e. ( M ... M ) <-> k = M ) )
6 velsn
 |-  ( k e. { M } <-> k = M )
7 5 6 bitr4di
 |-  ( M e. ZZ -> ( k e. ( M ... M ) <-> k e. { M } ) )
8 7 eqrdv
 |-  ( M e. ZZ -> ( M ... M ) = { M } )