Description: Membership in the set of positive reals. (Contributed by NM, 27Oct2007)
Ref  Expression  

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

1  breq2   ( x = A > ( 0 < x <> 0 < A ) ) 

2  dfrp   RR+ = { x e. RR  0 < x } 

3  1 2  elrab2   ( A e. RR+ <> ( A e. RR /\ 0 < A ) ) 