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

Theorem elrp 11778
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 4617 . 2 (𝑥 = 𝐴 → (0 < 𝑥 ↔ 0 < 𝐴))
2 df-rp 11777 . 2 + = {𝑥 ∈ ℝ ∣ 0 < 𝑥}
31, 2elrab2 3348 1 (𝐴 ∈ ℝ+ ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 384  wcel 1987   class class class wbr 4613  cr 9879  0cc0 9880   < clt 10018  +crp 11776
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-rab 2916  df-v 3188  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-nul 3892  df-if 4059  df-sn 4149  df-pr 4151  df-op 4155  df-br 4614  df-rp 11777
This theorem is referenced by:  elrpii  11779  nnrp  11786  rpgt0  11788  rpregt0  11790  ralrp  11796  rexrp  11797  rpaddcl  11798  rpmulcl  11799  rpdivcl  11800  rpgecl  11803  rphalflt  11804  ge0p1rp  11806  rpneg  11807  negelrp  11808  ltsubrp  11810  ltaddrp  11811  difrp  11812  elrpd  11813  infmrp1  12116  iccdil  12252  icccntr  12254  1mod  12642  expgt0  12833  resqrex  13925  sqrtdiv  13940  sqrtneglem  13941  mulcn2  14260  ef01bndlem  14839  sinltx  14844  met1stc  22236  met2ndci  22237  bcthlem4  23032  itg2mulc  23420  dvferm1  23652  dvne0  23678  reeff1o  24105  ellogdm  24285  cxpge0  24329  cxple2a  24345  cxpcn3lem  24388  cxpaddlelem  24392  cxpaddle  24393  atanbnd  24553  rlimcnp  24592  amgm  24617  chtub  24837  chebbnd1  25061  chto1ub  25065  pntlem3  25198  blocni  27509  dfrp2  29376  unbdqndv2lem2  32143  heiborlem8  33249  wallispilem4  39592  perfectALTVlem2  40926  regt1loggt0  41622
  Copyright terms: Public domain W3C validator