Theorem elrp 12960

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 5114	. 2 ⊢ (𝑥 = 𝐴 → (0 < 𝑥 ↔ 0 < 𝐴))
2		df-rp 12959	. 2 ⊢ ℝ+ = {𝑥 ∈ ℝ ∣ 0 < 𝑥}
3	1, 2	elrab2 3665	1 ⊢ (𝐴 ∈ ℝ+ ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴))

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2109   class class class wbr 5110  ℝcr 11074  0cc0 11075   < clt 11215  ℝ⁺crp 12958

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 2702

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 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-br 5111  df-rp 12959

This theorem is referenced by:  elrpii  12961  nnrp  12970  rpgt0  12971  rpregt0  12973  ralrp  12980  rexrp  12981  rpaddcl  12982  rpmulcl  12983  rpdivcl  12985  rpgecl  12988  rphalflt  12989  ge0p1rp  12991  rpneg  12992  negelrp  12993  ltsubrp  12996  ltaddrp  12997  difrp  12998  elrpd  12999  infmrp1  13312  dfrp2  13362  iccdil  13458  icccntr  13460  1mod  13872  expgt0  14067  resqrex  15223  sqrtdiv  15238  sqrtneglem  15239  mulcn2  15569  ef01bndlem  16159  sinltx  16164  met1stc  24416  met2ndci  24417  bcthlem4  25234  itg2mulc  25655  dvferm1  25896  dvne0  25923  reeff1o  26364  ellogdm  26555  cxpge0  26599  cxple2a  26615  cxpcn3lem  26664  cxpaddlelem  26668  cxpaddle  26669  atanbnd  26843  rlimcnp  26882  amgm  26908  chtub  27130  chebbnd1  27390  chto1ub  27394  pntlem3  27527  blocni  30741  rpdp2cl  32809  dp2ltc  32814  dplti  32832  dpgti  32833  dpexpp1  32835  dpmul4  32841  fdvposlt  34597  hgt750lem  34649  unbdqndv2lem2  36505  heiborlem8  37819  dvrelog2  42059  dvrelog3  42060  sqrtcvallem1  43627  wallispilem4  46073  perfectALTVlem2  47727  regt1loggt0  48529