Theorem fz0sn

Description: An integer range from 0 to 0 is a singleton. (Contributed by AV, 18-Apr-2021)

	Ref	Expression
Assertion	fz0sn	$$⊢\left(0\dots 0\right)=\left\{0\right\}$$

Proof

Step	Hyp	Ref	Expression
1		0z	$$⊢0\in \mathbb{Z}$$
2		fzsn	$$⊢0\in \mathbb{Z}\to \left(0\dots 0\right)=\left\{0\right\}$$
3	1 2	ax-mp	$$⊢\left(0\dots 0\right)=\left\{0\right\}$$