Theorem elrp 12732

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

Syntax hints:   ↔ wb 205   ∧ wa 396   ∈ wcel 2106   class class class wbr 5074  ℝcr 10870  0cc0 10871   < clt 11009  ℝ⁺crp 12730

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-br 5075  df-rp 12731

This theorem is referenced by:  elrpii  12733  nnrp  12741  rpgt0  12742  rpregt0  12744  ralrp  12750  rexrp  12751  rpaddcl  12752  rpmulcl  12753  rpdivcl  12755  rpgecl  12758  rphalflt  12759  ge0p1rp  12761  rpneg  12762  negelrp  12763  ltsubrp  12766  ltaddrp  12767  difrp  12768  elrpd  12769  infmrp1  13078  dfrp2  13128  iccdil  13222  icccntr  13224  1mod  13623  expgt0  13816  resqrex  14962  sqrtdiv  14977  sqrtneglem  14978  mulcn2  15305  ef01bndlem  15893  sinltx  15898  met1stc  23677  met2ndci  23678  bcthlem4  24491  itg2mulc  24912  dvferm1  25149  dvne0  25175  reeff1o  25606  ellogdm  25794  cxpge0  25838  cxple2a  25854  cxpcn3lem  25900  cxpaddlelem  25904  cxpaddle  25905  atanbnd  26076  rlimcnp  26115  amgm  26140  chtub  26360  chebbnd1  26620  chto1ub  26624  pntlem3  26757  blocni  29167  rpdp2cl  31156  dp2ltc  31161  dplti  31179  dpgti  31180  dpexpp1  31182  dpmul4  31188  fdvposlt  32579  hgt750lem  32631  unbdqndv2lem2  34690  heiborlem8  35976  dvrelog2  40072  dvrelog3  40073  2xp3dxp2ge1d  40162  sqrtcvallem1  41239  wallispilem4  43609  perfectALTVlem2  45174  regt1loggt0  45882