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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2114   class class class wbr 5086  ℝ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 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  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  24500  met2ndci  24501  bcthlem4  25308  itg2mulc  25728  dvferm1  25966  dvne0  25992  reeff1o  26429  ellogdm  26620  cxpge0  26664  cxple2a  26680  cxpcn3lem  26728  cxpaddlelem  26732  cxpaddle  26733  atanbnd  26907  rlimcnp  26946  amgm  26972  chtub  27193  chebbnd1  27453  chto1ub  27457  pntlem3  27590  blocni  30895  rpdp2cl  32960  dp2ltc  32965  dplti  32983  dpgti  32984  dpexpp1  32986  dpmul4  32992  fdvposlt  34763  hgt750lem  34815  unbdqndv2lem2  36790  heiborlem8  38157  dvrelog2  42521  dvrelog3  42522  sqrtcvallem1  44080  wallispilem4  46518  perfectALTVlem2  48214  regt1loggt0  49028