Metamath Proof Explorer


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 }