Theorem elrp 13008

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2108   class class class wbr 5119  ℝcr 11126  0cc0 11127   < clt 11267  ℝ⁺crp 13006

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 2707

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 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-br 5120  df-rp 13007

This theorem is referenced by:  elrpii  13009  nnrp  13018  rpgt0  13019  rpregt0  13021  ralrp  13027  rexrp  13028  rpaddcl  13029  rpmulcl  13030  rpdivcl  13032  rpgecl  13035  rphalflt  13036  ge0p1rp  13038  rpneg  13039  negelrp  13040  ltsubrp  13043  ltaddrp  13044  difrp  13045  elrpd  13046  infmrp1  13359  dfrp2  13409  iccdil  13505  icccntr  13507  1mod  13918  expgt0  14111  resqrex  15267  sqrtdiv  15282  sqrtneglem  15283  mulcn2  15610  ef01bndlem  16200  sinltx  16205  met1stc  24458  met2ndci  24459  bcthlem4  25277  itg2mulc  25698  dvferm1  25939  dvne0  25966  reeff1o  26407  ellogdm  26598  cxpge0  26642  cxple2a  26658  cxpcn3lem  26707  cxpaddlelem  26711  cxpaddle  26712  atanbnd  26886  rlimcnp  26925  amgm  26951  chtub  27173  chebbnd1  27433  chto1ub  27437  pntlem3  27570  blocni  30732  rpdp2cl  32802  dp2ltc  32807  dplti  32825  dpgti  32826  dpexpp1  32828  dpmul4  32834  fdvposlt  34577  hgt750lem  34629  unbdqndv2lem2  36474  heiborlem8  37788  dvrelog2  42023  dvrelog3  42024  2xp3dxp2ge1d  42200  sqrtcvallem1  43602  wallispilem4  46045  perfectALTVlem2  47684  regt1loggt0  48464