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 } )