Theorem elrp 12929

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.

Step	Hyp	Ref	Expression
1		breq2 5106	. 2 ⊢ (𝑥 = 𝐴 → (0 < 𝑥 ↔ 0 < 𝐴))
2		df-rp 12928	. 2 ⊢ ℝ+ = {𝑥 ∈ ℝ ∣ 0 < 𝑥}
3	1, 2	elrab2 3659	1 ⊢ (𝐴 ∈ ℝ+ ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴))

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2109   class class class wbr 5102  ℝcr 11043  0cc0 11044   < clt 11184  ℝ⁺crp 12927

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-br 5103  df-rp 12928

This theorem is referenced by:  elrpii  12930  nnrp  12939  rpgt0  12940  rpregt0  12942  ralrp  12949  rexrp  12950  rpaddcl  12951  rpmulcl  12952  rpdivcl  12954  rpgecl  12957  rphalflt  12958  ge0p1rp  12960  rpneg  12961  negelrp  12962  ltsubrp  12965  ltaddrp  12966  difrp  12967  elrpd  12968  infmrp1  13281  dfrp2  13331  iccdil  13427  icccntr  13429  1mod  13841  expgt0  14036  resqrex  15192  sqrtdiv  15207  sqrtneglem  15208  mulcn2  15538  ef01bndlem  16128  sinltx  16133  met1stc  24442  met2ndci  24443  bcthlem4  25260  itg2mulc  25681  dvferm1  25922  dvne0  25949  reeff1o  26390  ellogdm  26581  cxpge0  26625  cxple2a  26641  cxpcn3lem  26690  cxpaddlelem  26694  cxpaddle  26695  atanbnd  26869  rlimcnp  26908  amgm  26934  chtub  27156  chebbnd1  27416  chto1ub  27420  pntlem3  27553  blocni  30784  rpdp2cl  32852  dp2ltc  32857  dplti  32875  dpgti  32876  dpexpp1  32878  dpmul4  32884  fdvposlt  34583  hgt750lem  34635  unbdqndv2lem2  36491  heiborlem8  37805  dvrelog2  42045  dvrelog3  42046  sqrtcvallem1  43613  wallispilem4  46059  perfectALTVlem2  47716  regt1loggt0  48518