Theorem elrp 12139

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

Syntax hints:   ↔ wb 198   ∧ wa 386   ∈ wcel 2107   class class class wbr 4886  ℝcr 10271  0cc0 10272   < clt 10411  ℝ⁺crp 12137

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-rab 3099  df-v 3400  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-nul 4142  df-if 4308  df-sn 4399  df-pr 4401  df-op 4405  df-br 4887  df-rp 12138

This theorem is referenced by:  elrpii  12140  nnrp  12150  rpgt0  12151  rpregt0  12153  ralrp  12159  rexrp  12160  rpaddcl  12161  rpmulcl  12162  rpdivcl  12164  rpgecl  12167  rphalflt  12168  ge0p1rp  12170  rpneg  12171  negelrp  12172  ltsubrp  12175  ltaddrp  12176  difrp  12177  elrpd  12178  infmrp1  12486  iccdil  12627  icccntr  12629  1mod  13021  expgt0  13211  resqrex  14398  sqrtdiv  14413  sqrtneglem  14414  mulcn2  14734  ef01bndlem  15316  sinltx  15321  met1stc  22734  met2ndci  22735  bcthlem4  23533  itg2mulc  23951  dvferm1  24185  dvne0  24211  reeff1o  24638  ellogdm  24822  cxpge0  24866  cxple2a  24882  cxpcn3lem  24928  cxpaddlelem  24932  cxpaddle  24933  atanbnd  25104  rlimcnp  25144  amgm  25169  chtub  25389  chebbnd1  25613  chto1ub  25617  pntlem3  25750  blocni  28232  dfrp2  30097  rpdp2cl  30152  dp2ltc  30157  dplti  30175  dpgti  30176  dpexpp1  30178  dpmul4  30184  fdvposlt  31279  hgt750lem  31331  unbdqndv2lem2  33083  heiborlem8  34241  wallispilem4  41212  perfectALTVlem2  42656  regt1loggt0  43345