Theorem fz0sn

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

	Ref	Expression
Assertion	fz0sn	⊢ ( 0 ... 0 ) = { 0 }

Proof

Step	Hyp	Ref	Expression
1		0z	⊢ 0 ∈ ℤ
2		fzsn	⊢ ( 0 ∈ ℤ → ( 0 ... 0 ) = { 0 } )
3	1 2	ax-mp	⊢ ( 0 ... 0 ) = { 0 }