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 ( 𝐴 ∈ ℤ → ( 𝐴 ..^ ( 𝐴 + 1 ) ) = { 𝐴 } )

Proof

Step Hyp Ref Expression
1 fzval3 ( 𝐴 ∈ ℤ → ( 𝐴 ... 𝐴 ) = ( 𝐴 ..^ ( 𝐴 + 1 ) ) )
2 fzsn ( 𝐴 ∈ ℤ → ( 𝐴 ... 𝐴 ) = { 𝐴 } )
3 1 2 eqtr3d ( 𝐴 ∈ ℤ → ( 𝐴 ..^ ( 𝐴 + 1 ) ) = { 𝐴 } )