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

Theorem elrp 10614
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 4216 . 2  |-  ( x  =  A  ->  (
0  <  x  <->  0  <  A ) )
2 df-rp 10613 . 2  |-  RR+  =  { x  e.  RR  |  0  <  x }
31, 2elrab2 3094 1  |-  ( A  e.  RR+  <->  ( A  e.  RR  /\  0  < 
A ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    /\ wa 359    e. wcel 1725   class class class wbr 4212   RRcr 8989   0cc0 8990    < clt 9120   RR+crp 10612
This theorem is referenced by:  elrpii  10615  nnrp  10621  rpgt0  10623  rpregt0  10625  ralrp  10630  rexrp  10631  rpaddcl  10632  rpmulcl  10633  rpdivcl  10634  rpgecl  10637  rphalflt  10638  ge0p1rp  10640  rpneg  10641  ltsubrp  10643  ltaddrp  10644  difrp  10645  elrpd  10646  iccdil  11034  icccntr  11036  1mod  11273  expgt0  11413  resqrex  12056  sqrdiv  12071  sqrneglem  12072  mulcn2  12389  ef01bndlem  12785  sinltx  12790  met1stc  18551  met2ndci  18552  bcthlem4  19280  itg2mulc  19639  dvferm1  19869  dvne0  19895  reeff1o  20363  ellogdm  20530  cxpge0  20574  cxple2a  20590  cxpcn3lem  20631  cxpaddlelem  20635  cxpaddle  20636  atanbnd  20766  rlimcnp  20804  amgm  20829  chtub  20996  chebbnd1  21166  chto1ub  21170  pntlem3  21303  blocni  22306  heiborlem8  26527  wallispilem4  27793
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-rab 2714  df-v 2958  df-dif 3323  df-un 3325  df-in 3327  df-ss 3334  df-nul 3629  df-if 3740  df-sn 3820  df-pr 3821  df-op 3823  df-br 4213  df-rp 10613
  Copyright terms: Public domain W3C validator