Metamath Proof Explorer


Theorem ioorp

Description: The set of positive reals expressed as an open interval. (Contributed by Steve Rodriguez, 25-Nov-2007)

Ref Expression
Assertion ioorp
|- ( 0 (,) +oo ) = RR+

Proof

Step Hyp Ref Expression
1 ioopos
 |-  ( 0 (,) +oo ) = { x e. RR | 0 < x }
2 df-rp
 |-  RR+ = { x e. RR | 0 < x }
3 1 2 eqtr4i
 |-  ( 0 (,) +oo ) = RR+