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

Theorem elrp 12383
Description: Membership in the set of positive reals. (Contributed by NM, 27-Oct-2007.)
Assertion
Ref Expression
elrp (𝐴 ∈ ℝ+ ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴))

Proof of Theorem elrp
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 breq2 5061 . 2 (𝑥 = 𝐴 → (0 < 𝑥 ↔ 0 < 𝐴))
2 df-rp 12382 . 2 + = {𝑥 ∈ ℝ ∣ 0 < 𝑥}
31, 2elrab2 3681 1 (𝐴 ∈ ℝ+ ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴))
Colors of variables: wff setvar class
Syntax hints:  wb 208  wa 398  wcel 2108   class class class wbr 5057  cr 10528  0cc0 10529   < clt 10667  +crp 12381
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2154  ax-12 2170  ax-ext 2791
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1084  df-tru 1534  df-ex 1775  df-nf 1779  df-sb 2064  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-rab 3145  df-v 3495  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-nul 4290  df-if 4466  df-sn 4560  df-pr 4562  df-op 4566  df-br 5058  df-rp 12382
This theorem is referenced by:  elrpii  12384  nnrp  12392  rpgt0  12393  rpregt0  12395  ralrp  12401  rexrp  12402  rpaddcl  12403  rpmulcl  12404  rpdivcl  12406  rpgecl  12409  rphalflt  12410  ge0p1rp  12412  rpneg  12413  negelrp  12414  ltsubrp  12417  ltaddrp  12418  difrp  12419  elrpd  12420  infmrp1  12729  iccdil  12868  icccntr  12870  1mod  13263  expgt0  13454  resqrex  14602  sqrtdiv  14617  sqrtneglem  14618  mulcn2  14944  ef01bndlem  15529  sinltx  15534  met1stc  23123  met2ndci  23124  bcthlem4  23922  itg2mulc  24340  dvferm1  24574  dvne0  24600  reeff1o  25027  ellogdm  25214  cxpge0  25258  cxple2a  25274  cxpcn3lem  25320  cxpaddlelem  25324  cxpaddle  25325  atanbnd  25496  rlimcnp  25535  amgm  25560  chtub  25780  chebbnd1  26040  chto1ub  26044  pntlem3  26177  blocni  28574  dfrp2  30483  rpdp2cl  30551  dp2ltc  30556  dplti  30574  dpgti  30575  dpexpp1  30577  dpmul4  30583  fdvposlt  31863  hgt750lem  31915  unbdqndv2lem2  33842  heiborlem8  35088  wallispilem4  42343  perfectALTVlem2  43877  regt1loggt0  44586
  Copyright terms: Public domain W3C validator