Theorem elrp 12997

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

Syntax hints:   ↔ wb 208   ∧ wa 399   ∈ wcel 2144   class class class wbr 5102  ℝcr 11074  0cc0 11075   < clt 11218  ℝ⁺crp 12995

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1101  df-tru 1565  df-fal 1575  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-rab 3417  df-v 3458  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4288  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5103  df-rp 12996

This theorem is referenced by:  elrpii  12998  nnrp  13007  rpgt0  13008  rpregt0  13010  ralrp  13017  rexrp  13018  rpaddcl  13019  rpmulcl  13020  rpdivcl  13022  rpgecl  13025  rphalflt  13026  ge0p1rp  13028  rpneg  13029  negelrp  13030  ltsubrp  13033  ltaddrp  13034  difrp  13035  elrpd  13036  infmrp1  13350  dfrp2  13400  iccdil  13496  icccntr  13498  1mod  13915  expgt0  14110  resqrex  15279  sqrtdiv  15294  sqrtneglem  15295  mulcn2  15625  ef01bndlem  16218  sinltx  16223  met1stc  24583  met2ndci  24584  bcthlem4  25391  itg2mulc  25811  dvferm1  26049  dvne0  26075  reeff1o  26512  ellogdm  26706  cxpge0  26750  cxple2a  26766  cxpcn3lem  26814  cxpaddlelem  26818  cxpaddle  26819  atanbnd  26993  rlimcnp  27032  amgm  27057  chtub  27278  chebbnd1  27538  chto1ub  27542  pntlem3  27675  blocni  31010  rpdp2cl  33061  dp2ltc  33066  dplti  33084  dpgti  33085  dpexpp1  33087  dpmul4  33093  fdvposlt  34895  hgt750lem  34947  unbdqndv2lem2  36953  heiborlem8  38322  dvrelog2  42686  dvrelog3  42687  sqrtcvallem1  44212  wallispilem4  46647  perfectALTVlem2  48349  regt1loggt0  49163