Theorem elrp 12661

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

Syntax hints:   ↔ wb 205   ∧ wa 395   ∈ wcel 2108   class class class wbr 5070  ℝcr 10801  0cc0 10802   < clt 10940  ℝ⁺crp 12659

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-br 5071  df-rp 12660

This theorem is referenced by:  elrpii  12662  nnrp  12670  rpgt0  12671  rpregt0  12673  ralrp  12679  rexrp  12680  rpaddcl  12681  rpmulcl  12682  rpdivcl  12684  rpgecl  12687  rphalflt  12688  ge0p1rp  12690  rpneg  12691  negelrp  12692  ltsubrp  12695  ltaddrp  12696  difrp  12697  elrpd  12698  infmrp1  13007  dfrp2  13057  iccdil  13151  icccntr  13153  1mod  13551  expgt0  13744  resqrex  14890  sqrtdiv  14905  sqrtneglem  14906  mulcn2  15233  ef01bndlem  15821  sinltx  15826  met1stc  23583  met2ndci  23584  bcthlem4  24396  itg2mulc  24817  dvferm1  25054  dvne0  25080  reeff1o  25511  ellogdm  25699  cxpge0  25743  cxple2a  25759  cxpcn3lem  25805  cxpaddlelem  25809  cxpaddle  25810  atanbnd  25981  rlimcnp  26020  amgm  26045  chtub  26265  chebbnd1  26525  chto1ub  26529  pntlem3  26662  blocni  29068  rpdp2cl  31058  dp2ltc  31063  dplti  31081  dpgti  31082  dpexpp1  31084  dpmul4  31090  fdvposlt  32479  hgt750lem  32531  unbdqndv2lem2  34617  heiborlem8  35903  dvrelog2  40000  dvrelog3  40001  2xp3dxp2ge1d  40090  sqrtcvallem1  41128  wallispilem4  43499  perfectALTVlem2  45062  regt1loggt0  45770