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

Syntax hints:   ↔ wb 209   ∧ wa 400   ∈ wcel 2149   class class class wbr 5111  ℝcr 11099  0cc0 11100   < clt 11243  ℝ⁺crp 13016

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3423  df-v 3463  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4491  df-sn 4593  df-pr 4595  df-op 4599  df-br 5112  df-rp 13017

This theorem is referenced by:  elrpii  13019  nnrp  13028  rpgt0  13029  rpregt0  13031  ralrp  13038  rexrp  13039  rpaddcl  13040  rpmulcl  13041  rpdivcl  13043  rpgecl  13046  rphalflt  13047  ge0p1rp  13049  rpneg  13050  negelrp  13051  ltsubrp  13054  ltaddrp  13055  difrp  13056  elrpd  13057  infmrp1  13371  dfrp2  13421  iccdil  13517  icccntr  13519  1mod  13936  expgt0  14131  resqrex  15301  sqrtdiv  15316  sqrtneglem  15317  mulcn2  15647  ef01bndlem  16240  sinltx  16245  met1stc  24647  met2ndci  24648  bcthlem4  25455  itg2mulc  25875  dvferm1  26113  dvne0  26139  reeff1o  26576  ellogdm  26770  cxpge0  26814  cxple2a  26830  cxpcn3lem  26878  cxpaddlelem  26882  cxpaddle  26883  atanbnd  27057  rlimcnp  27096  amgm  27121  chtub  27342  chebbnd1  27602  chto1ub  27606  pntlem3  27739  blocni  31098  rpdp2cl  33142  dp2ltc  33147  dplti  33165  dpgti  33166  dpexpp1  33168  dpmul4  33174  fdvposlt  34931  hgt750lem  34983  unbdqndv2lem2  37022  heiborlem8  38392  dvrelog2  42756  dvrelog3  42757  sqrtcvallem1  44284  wallispilem4  46709  perfectALTVlem2  48411  regt1loggt0  49236