Theorem elrp 12976

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

Syntax hints:   ↔ wb 205   ∧ wa 397   ∈ wcel 2107   class class class wbr 5149  ℝcr 11109  0cc0 11110   < clt 11248  ℝ⁺crp 12974

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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-br 5150  df-rp 12975

This theorem is referenced by:  elrpii  12977  nnrp  12985  rpgt0  12986  rpregt0  12988  ralrp  12994  rexrp  12995  rpaddcl  12996  rpmulcl  12997  rpdivcl  12999  rpgecl  13002  rphalflt  13003  ge0p1rp  13005  rpneg  13006  negelrp  13007  ltsubrp  13010  ltaddrp  13011  difrp  13012  elrpd  13013  infmrp1  13323  dfrp2  13373  iccdil  13467  icccntr  13469  1mod  13868  expgt0  14061  resqrex  15197  sqrtdiv  15212  sqrtneglem  15213  mulcn2  15540  ef01bndlem  16127  sinltx  16132  met1stc  24030  met2ndci  24031  bcthlem4  24844  itg2mulc  25265  dvferm1  25502  dvne0  25528  reeff1o  25959  ellogdm  26147  cxpge0  26191  cxple2a  26207  cxpcn3lem  26255  cxpaddlelem  26259  cxpaddle  26260  atanbnd  26431  rlimcnp  26470  amgm  26495  chtub  26715  chebbnd1  26975  chto1ub  26979  pntlem3  27112  blocni  30058  rpdp2cl  32048  dp2ltc  32053  dplti  32071  dpgti  32072  dpexpp1  32074  dpmul4  32080  fdvposlt  33611  hgt750lem  33663  unbdqndv2lem2  35386  heiborlem8  36686  dvrelog2  40929  dvrelog3  40930  2xp3dxp2ge1d  41022  sqrtcvallem1  42382  wallispilem4  44784  perfectALTVlem2  46390  regt1loggt0  47222