Theorem elrp 13046

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   ∈ wcel 2145   class class class wbr 5107  ℝcr 11126  0cc0 11127   < clt 11270  ℝ⁺crp 13044

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-br 5108  df-rp 13045

This theorem is used by:  elrpii  13047  nnrp  13056  rpgt0  13057  rpregt0  13059  ralrp  13066  rexrp  13067  rpaddcl  13068  rpmulcl  13069  rpdivcl  13071  rpgecl  13074  rphalflt  13075  ge0p1rp  13077  rpneg  13078  negelrp  13079  ltsubrp  13082  ltaddrp  13083  difrp  13084  elrpd  13085  infmrp1  13399  dfrp2  13449  iccdil  13545  icccntr  13547  1mod  13966  expgt0  14161  resqrex  15339  sqrtdiv  15354  sqrtneglem  15355  mulcn2  15685  ef01bndlem  16276  sinltx  16281  met1stc  24748  met2ndci  24749  bcthlem4  25556  itg2mulc  25976  dvferm1  26214  dvne0  26240  reeff1o  26680  ellogdm  26874  cxpge0  26918  cxple2a  26934  cxpcn3lem  26982  cxpaddlelem  26986  cxpaddle  26987  atanbnd  27161  rlimcnp  27200  amgm  27225  chtub  27446  chebbnd1  27706  chto1ub  27710  pntlem3  27843  blocni  31272  rpdp2cl  33314  dp2ltc  33319  dplti  33337  dpgti  33338  dpexpp1  33340  dpmul4  33346  fdvposlt  35094  hgt750lem  35146  unbdqndv2lem2  37194  heiborlem8  38555  dvrelog2  42917  dvrelog3  42918  sqrtcvallem1  44458  wallispilem4  46883  perfectALTVlem2  48625  regt1loggt0  49453