fzsn

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

		Ref	Expression
	Assertion	fzsn	$⊢ M \in ℤ \to (M \dots M) = \{M\}$

Step	Hyp	Ref	Expression
1		elfz1eq	$⊢ k \in (M \dots M) \to k = M$
2		elfz3	$⊢ M \in ℤ \to M \in (M \dots M)$
3		eleq1	$⊢ k = M \to (k \in (M \dots M) \leftrightarrow M \in (M \dots M))$
4	2 3	syl5ibrcom	$⊢ M \in ℤ \to (k = M \to k \in (M \dots M))$
5	1 4	impbid2	$⊢ M \in ℤ \to (k \in (M \dots M) \leftrightarrow k = M)$
6		velsn	$⊢ k \in \{M\} \leftrightarrow k = M$
7	5 6	bitr4di	$⊢ M \in ℤ \to (k \in (M \dots M) \leftrightarrow k \in \{M\})$
8	7	eqrdv	$⊢ M \in ℤ \to (M \dots M) = \{M\}$

Metamath Proof Explorer