Theorem elrp 12892

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2111   class class class wbr 5089  ℝcr 11005  0cc0 11006   < clt 11146  ℝ⁺crp 12890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580  df-br 5090  df-rp 12891

This theorem is referenced by:  elrpii  12893  nnrp  12902  rpgt0  12903  rpregt0  12905  ralrp  12912  rexrp  12913  rpaddcl  12914  rpmulcl  12915  rpdivcl  12917  rpgecl  12920  rphalflt  12921  ge0p1rp  12923  rpneg  12924  negelrp  12925  ltsubrp  12928  ltaddrp  12929  difrp  12930  elrpd  12931  infmrp1  13244  dfrp2  13294  iccdil  13390  icccntr  13392  1mod  13807  expgt0  14002  resqrex  15157  sqrtdiv  15172  sqrtneglem  15173  mulcn2  15503  ef01bndlem  16093  sinltx  16098  met1stc  24436  met2ndci  24437  bcthlem4  25254  itg2mulc  25675  dvferm1  25916  dvne0  25943  reeff1o  26384  ellogdm  26575  cxpge0  26619  cxple2a  26635  cxpcn3lem  26684  cxpaddlelem  26688  cxpaddle  26689  atanbnd  26863  rlimcnp  26902  amgm  26928  chtub  27150  chebbnd1  27410  chto1ub  27414  pntlem3  27547  blocni  30785  rpdp2cl  32862  dp2ltc  32867  dplti  32885  dpgti  32886  dpexpp1  32888  dpmul4  32894  fdvposlt  34612  hgt750lem  34664  unbdqndv2lem2  36554  heiborlem8  37857  dvrelog2  42156  dvrelog3  42157  sqrtcvallem1  43723  wallispilem4  46165  perfectALTVlem2  47821  regt1loggt0  48636