Metamath Proof Explorer

Theorem elrpii

Description: Membership in the set of positive reals. (Contributed by NM, 23-Feb-2008)

Ref Expression
Hypotheses elrpi.1 
|- A e. RR
elrpi.2 
|- 0 < A
Assertion elrpii 
|- A e. RR+

Proof

Step Hyp Ref Expression
1 elrpi.1 
 |-  A e. RR
2 elrpi.2 
 |-  0 < A
3 elrp 
 |-  ( A e. RR+ <-> ( A e. RR /\ 0 < A ) )
4 1 2 3 mpbir2an 
 |-  A e. RR+