Theorem elrp 12905

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2113   class class class wbr 5096  ℝcr 11023  0cc0 11024   < clt 11164  ℝ⁺crp 12903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-br 5097  df-rp 12904

This theorem is referenced by:  elrpii  12906  nnrp  12915  rpgt0  12916  rpregt0  12918  ralrp  12925  rexrp  12926  rpaddcl  12927  rpmulcl  12928  rpdivcl  12930  rpgecl  12933  rphalflt  12934  ge0p1rp  12936  rpneg  12937  negelrp  12938  ltsubrp  12941  ltaddrp  12942  difrp  12943  elrpd  12944  infmrp1  13258  dfrp2  13308  iccdil  13404  icccntr  13406  1mod  13821  expgt0  14016  resqrex  15171  sqrtdiv  15186  sqrtneglem  15187  mulcn2  15517  ef01bndlem  16107  sinltx  16112  met1stc  24463  met2ndci  24464  bcthlem4  25281  itg2mulc  25702  dvferm1  25943  dvne0  25970  reeff1o  26411  ellogdm  26602  cxpge0  26646  cxple2a  26662  cxpcn3lem  26711  cxpaddlelem  26715  cxpaddle  26716  atanbnd  26890  rlimcnp  26929  amgm  26955  chtub  27177  chebbnd1  27437  chto1ub  27441  pntlem3  27574  blocni  30829  rpdp2cl  32912  dp2ltc  32917  dplti  32935  dpgti  32936  dpexpp1  32938  dpmul4  32944  fdvposlt  34705  hgt750lem  34757  unbdqndv2lem2  36653  heiborlem8  37958  dvrelog2  42257  dvrelog3  42258  sqrtcvallem1  43814  wallispilem4  46254  perfectALTVlem2  47910  regt1loggt0  48724