Theorem elrp 13036

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2108   class class class wbr 5143  ℝcr 11154  0cc0 11155   < clt 11295  ℝ⁺crp 13034

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-br 5144  df-rp 13035

This theorem is referenced by:  elrpii  13037  nnrp  13046  rpgt0  13047  rpregt0  13049  ralrp  13055  rexrp  13056  rpaddcl  13057  rpmulcl  13058  rpdivcl  13060  rpgecl  13063  rphalflt  13064  ge0p1rp  13066  rpneg  13067  negelrp  13068  ltsubrp  13071  ltaddrp  13072  difrp  13073  elrpd  13074  infmrp1  13386  dfrp2  13436  iccdil  13530  icccntr  13532  1mod  13943  expgt0  14136  resqrex  15289  sqrtdiv  15304  sqrtneglem  15305  mulcn2  15632  ef01bndlem  16220  sinltx  16225  met1stc  24534  met2ndci  24535  bcthlem4  25361  itg2mulc  25782  dvferm1  26023  dvne0  26050  reeff1o  26491  ellogdm  26681  cxpge0  26725  cxple2a  26741  cxpcn3lem  26790  cxpaddlelem  26794  cxpaddle  26795  atanbnd  26969  rlimcnp  27008  amgm  27034  chtub  27256  chebbnd1  27516  chto1ub  27520  pntlem3  27653  blocni  30824  rpdp2cl  32864  dp2ltc  32869  dplti  32887  dpgti  32888  dpexpp1  32890  dpmul4  32896  fdvposlt  34614  hgt750lem  34666  unbdqndv2lem2  36511  heiborlem8  37825  dvrelog2  42065  dvrelog3  42066  2xp3dxp2ge1d  42242  sqrtcvallem1  43644  wallispilem4  46083  perfectALTVlem2  47709  regt1loggt0  48457