MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elrp Unicode version

Theorem elrp 10372
Description: Membership in the set of positive reals. (Contributed by NM, 27-Oct-2007.)
Assertion
Ref Expression
elrp  |-  ( A  e.  RR+  <->  ( A  e.  RR  /\  0  < 
A ) )

Proof of Theorem elrp
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 breq2 4043 . 2  |-  ( x  =  A  ->  (
0  <  x  <->  0  <  A ) )
2 df-rp 10371 . 2  |-  RR+  =  { x  e.  RR  |  0  <  x }
31, 2elrab2 2938 1  |-  ( A  e.  RR+  <->  ( A  e.  RR  /\  0  < 
A ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    /\ wa 358    e. wcel 1696   class class class wbr 4039   RRcr 8752   0cc0 8753    < clt 8883   RR+crp 10370
This theorem is referenced by:  elrpii  10373  nnrp  10379  rpgt0  10381  rpregt0  10383  ralrp  10388  rexrp  10389  rpaddcl  10390  rpmulcl  10391  rpdivcl  10392  rpgecl  10395  rphalflt  10396  ge0p1rp  10398  rpneg  10399  ltsubrp  10401  ltaddrp  10402  difrp  10403  elrpd  10404  iccdil  10789  icccntr  10791  1mod  11012  expgt0  11151  resqrex  11752  sqrdiv  11767  sqrneglem  11768  mulcn2  12085  ef01bndlem  12480  sinltx  12485  met1stc  18083  met2ndci  18084  bcthlem4  18765  itg2mulc  19118  dvferm1  19348  dvne0  19374  reeff1o  19839  ellogdm  20002  cxpge0  20046  cxple2a  20062  cxpcn3lem  20103  cxpaddlelem  20107  cxpaddle  20108  atanbnd  20238  rlimcnp  20276  amgm  20301  chtub  20467  chebbnd1  20637  chto1ub  20641  pntlem3  20774  blocni  21399  probmeasb  23648  cndprobprob  23656  heiborlem8  26645  stoweidlem5  27857  stoweidlem25  27877  stoweidlem28  27880  stoweidlem42  27894  stoweidlem49  27901  stoweidlem59  27911  stoweid  27915  wallispilem3  27919  wallispilem4  27920  wallispi  27922  wallispi2lem1  27923
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-rab 2565  df-v 2803  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662  df-br 4040  df-rp 10371
  Copyright terms: Public domain W3C validator