Metamath Proof Explorer

Theorem repos

Description: Two ways of saying that a real number is positive. (Contributed by NM, 7-May-2007)

Ref Expression
Assertion repos 
|- ( A e. ( 0 (,) +oo ) <-> ( A e. RR /\ 0 < A ) )

Proof

Step Hyp Ref Expression
1 breq2 
 |-  ( x = A -> ( 0 < x <-> 0 < A ) )
2 ioopos 
 |-  ( 0 (,) +oo ) = { x e. RR | 0 < x }
3 1 2 elrab2 
 |-  ( A e. ( 0 (,) +oo ) <-> ( A e. RR /\ 0 < A ) )