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

Theorem elrp 10356
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 4027 . 2  |-  ( x  =  A  ->  (
0  <  x  <->  0  <  A ) )
2 df-rp 10355 . 2  |-  RR+  =  { x  e.  RR  |  0  <  x }
31, 2elrab2 2925 1  |-  ( A  e.  RR+  <->  ( A  e.  RR  /\  0  < 
A ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    /\ wa 358    e. wcel 1684   class class class wbr 4023   RRcr 8736   0cc0 8737    < clt 8867   RR+crp 10354
This theorem is referenced by:  elrpii  10357  nnrp  10363  rpgt0  10365  rpregt0  10367  ralrp  10372  rexrp  10373  rpaddcl  10374  rpmulcl  10375  rpdivcl  10376  rpgecl  10379  rphalflt  10380  ge0p1rp  10382  rpneg  10383  ltsubrp  10385  ltaddrp  10386  difrp  10387  elrpd  10388  iccdil  10773  icccntr  10775  1mod  10996  expgt0  11135  resqrex  11736  sqrdiv  11751  sqrneglem  11752  mulcn2  12069  ef01bndlem  12464  sinltx  12469  met1stc  18067  met2ndci  18068  bcthlem4  18749  itg2mulc  19102  dvferm1  19332  dvne0  19358  reeff1o  19823  ellogdm  19986  cxpge0  20030  cxple2a  20046  cxpcn3lem  20087  cxpaddlelem  20091  cxpaddle  20092  atanbnd  20222  rlimcnp  20260  amgm  20285  chtub  20451  chebbnd1  20621  chto1ub  20625  pntlem3  20758  blocni  21383  probmeasb  23633  cndprobprob  23641  heiborlem8  26542  stoweidlem5  27754  stoweidlem25  27774  stoweidlem28  27777  stoweidlem42  27791  stoweidlem49  27798  stoweidlem59  27808  stoweid  27812  wallispilem3  27816  wallispilem4  27817  wallispi  27819  wallispi2lem1  27820
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-br 4024  df-rp 10355
  Copyright terms: Public domain W3C validator