Metamath Proof Explorer

Theorem elrp

Description: Membership in the set of positive reals. (Contributed by NM, 27-Oct-2007)

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

Proof

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