Metamath Proof Explorer

Theorem fzosn

Description: Expressing a singleton as a half-open range. (Contributed by Stefan O'Rear, 23-Aug-2015)

Ref Expression
Assertion fzosn 
|- ( A e. ZZ -> ( A ..^ ( A + 1 ) ) = { A } )

Proof

Step Hyp Ref Expression
1 fzval3 
 |-  ( A e. ZZ -> ( A ... A ) = ( A ..^ ( A + 1 ) ) )
2 fzsn 
 |-  ( A e. ZZ -> ( A ... A ) = { A } )
3 1 2 eqtr3d 
 |-  ( A e. ZZ -> ( A ..^ ( A + 1 ) ) = { A } )