Theorem elrp 12939

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

Syntax hints:   ↔ wb 208   ∧ wa 397   ∈ wcel 2121   class class class wbr 5075  ℝcr 11032  0cc0 11033   < clt 11174  ℝ⁺crp 12937

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-rab 3394  df-v 3435  df-dif 3888  df-un 3890  df-ss 3902  df-nul 4265  df-if 4458  df-sn 4559  df-pr 4561  df-op 4565  df-br 5076  df-rp 12938

This theorem is referenced by:  elrpii  12940  nnrp  12949  rpgt0  12950  rpregt0  12952  ralrp  12959  rexrp  12960  rpaddcl  12961  rpmulcl  12962  rpdivcl  12964  rpgecl  12967  rphalflt  12968  ge0p1rp  12970  rpneg  12971  negelrp  12972  ltsubrp  12975  ltaddrp  12976  difrp  12977  elrpd  12978  infmrp1  13292  dfrp2  13342  iccdil  13438  icccntr  13440  1mod  13857  expgt0  14052  resqrex  15207  sqrtdiv  15222  sqrtneglem  15223  mulcn2  15553  ef01bndlem  16146  sinltx  16151  met1stc  24508  met2ndci  24509  bcthlem4  25316  itg2mulc  25736  dvferm1  25974  dvne0  26000  reeff1o  26434  ellogdm  26625  cxpge0  26669  cxple2a  26685  cxpcn3lem  26733  cxpaddlelem  26737  cxpaddle  26738  atanbnd  26912  rlimcnp  26951  amgm  26976  chtub  27197  chebbnd1  27457  chto1ub  27461  pntlem3  27594  blocni  30898  rpdp2cl  32964  dp2ltc  32969  dplti  32987  dpgti  32988  dpexpp1  32990  dpmul4  32996  fdvposlt  34795  hgt750lem  34847  unbdqndv2lem2  36831  heiborlem8  38200  dvrelog2  42564  dvrelog3  42565  sqrtcvallem1  44090  wallispilem4  46525  perfectALTVlem2  48227  regt1loggt0  49041