Theorem elrp 12895

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2109   class class class wbr 5092  ℝcr 11008  0cc0 11009   < clt 11149  ℝ⁺crp 12893

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 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5093  df-rp 12894

This theorem is referenced by:  elrpii  12896  nnrp  12905  rpgt0  12906  rpregt0  12908  ralrp  12915  rexrp  12916  rpaddcl  12917  rpmulcl  12918  rpdivcl  12920  rpgecl  12923  rphalflt  12924  ge0p1rp  12926  rpneg  12927  negelrp  12928  ltsubrp  12931  ltaddrp  12932  difrp  12933  elrpd  12934  infmrp1  13247  dfrp2  13297  iccdil  13393  icccntr  13395  1mod  13807  expgt0  14002  resqrex  15157  sqrtdiv  15172  sqrtneglem  15173  mulcn2  15503  ef01bndlem  16093  sinltx  16098  met1stc  24407  met2ndci  24408  bcthlem4  25225  itg2mulc  25646  dvferm1  25887  dvne0  25914  reeff1o  26355  ellogdm  26546  cxpge0  26590  cxple2a  26606  cxpcn3lem  26655  cxpaddlelem  26659  cxpaddle  26660  atanbnd  26834  rlimcnp  26873  amgm  26899  chtub  27121  chebbnd1  27381  chto1ub  27385  pntlem3  27518  blocni  30749  rpdp2cl  32823  dp2ltc  32828  dplti  32846  dpgti  32847  dpexpp1  32849  dpmul4  32855  fdvposlt  34573  hgt750lem  34625  unbdqndv2lem2  36494  heiborlem8  37808  dvrelog2  42047  dvrelog3  42048  sqrtcvallem1  43614  wallispilem4  46059  perfectALTVlem2  47716  regt1loggt0  48531