Theorem elrp 13033

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2105   class class class wbr 5147  ℝcr 11151  0cc0 11152   < clt 11292  ℝ⁺crp 13031

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-br 5148  df-rp 13032

This theorem is referenced by:  elrpii  13034  nnrp  13043  rpgt0  13044  rpregt0  13046  ralrp  13052  rexrp  13053  rpaddcl  13054  rpmulcl  13055  rpdivcl  13057  rpgecl  13060  rphalflt  13061  ge0p1rp  13063  rpneg  13064  negelrp  13065  ltsubrp  13068  ltaddrp  13069  difrp  13070  elrpd  13071  infmrp1  13382  dfrp2  13432  iccdil  13526  icccntr  13528  1mod  13939  expgt0  14132  resqrex  15285  sqrtdiv  15300  sqrtneglem  15301  mulcn2  15628  ef01bndlem  16216  sinltx  16221  met1stc  24549  met2ndci  24550  bcthlem4  25374  itg2mulc  25796  dvferm1  26037  dvne0  26064  reeff1o  26505  ellogdm  26695  cxpge0  26739  cxple2a  26755  cxpcn3lem  26804  cxpaddlelem  26808  cxpaddle  26809  atanbnd  26983  rlimcnp  27022  amgm  27048  chtub  27270  chebbnd1  27530  chto1ub  27534  pntlem3  27667  blocni  30833  rpdp2cl  32848  dp2ltc  32853  dplti  32871  dpgti  32872  dpexpp1  32874  dpmul4  32880  fdvposlt  34592  hgt750lem  34644  unbdqndv2lem2  36492  heiborlem8  37804  dvrelog2  42045  dvrelog3  42046  2xp3dxp2ge1d  42222  sqrtcvallem1  43620  wallispilem4  46023  perfectALTVlem2  47646  regt1loggt0  48385