Theorem elrp 13018

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2107   class class class wbr 5123  ℝcr 11136  0cc0 11137   < clt 11277  ℝ⁺crp 13016

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-rab 3420  df-v 3465  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-br 5124  df-rp 13017

This theorem is referenced by:  elrpii  13019  nnrp  13028  rpgt0  13029  rpregt0  13031  ralrp  13037  rexrp  13038  rpaddcl  13039  rpmulcl  13040  rpdivcl  13042  rpgecl  13045  rphalflt  13046  ge0p1rp  13048  rpneg  13049  negelrp  13050  ltsubrp  13053  ltaddrp  13054  difrp  13055  elrpd  13056  infmrp1  13368  dfrp2  13418  iccdil  13512  icccntr  13514  1mod  13925  expgt0  14118  resqrex  15272  sqrtdiv  15287  sqrtneglem  15288  mulcn2  15615  ef01bndlem  16203  sinltx  16208  met1stc  24479  met2ndci  24480  bcthlem4  25298  itg2mulc  25719  dvferm1  25960  dvne0  25987  reeff1o  26428  ellogdm  26618  cxpge0  26662  cxple2a  26678  cxpcn3lem  26727  cxpaddlelem  26731  cxpaddle  26732  atanbnd  26906  rlimcnp  26945  amgm  26971  chtub  27193  chebbnd1  27453  chto1ub  27457  pntlem3  27590  blocni  30753  rpdp2cl  32809  dp2ltc  32814  dplti  32832  dpgti  32833  dpexpp1  32835  dpmul4  32841  fdvposlt  34589  hgt750lem  34641  unbdqndv2lem2  36486  heiborlem8  37800  dvrelog2  42040  dvrelog3  42041  2xp3dxp2ge1d  42217  sqrtcvallem1  43621  wallispilem4  46055  perfectALTVlem2  47682  regt1loggt0  48430