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 AA..^A+1=A

Proof

Step Hyp Ref Expression
1 fzval3 AAA=A..^A+1
2 fzsn AAA=A
3 1 2 eqtr3d AA..^A+1=A