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 e. ZZ
2 fzsn 
 |-  ( 0 e. ZZ -> ( 0 ... 0 ) = { 0 } )
3 1 2 ax-mp 
 |-  ( 0 ... 0 ) = { 0 }