Theorem elrp 12379

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

Syntax hints:   ↔ wb 209   ∧ wa 399   ∈ wcel 2111   class class class wbr 5030  ℝcr 10525  0cc0 10526   < clt 10664  ℝ⁺crp 12377

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-rab 3115  df-v 3443  df-un 3886  df-sn 4526  df-pr 4528  df-op 4532  df-br 5031  df-rp 12378

This theorem is referenced by:  elrpii  12380  nnrp  12388  rpgt0  12389  rpregt0  12391  ralrp  12397  rexrp  12398  rpaddcl  12399  rpmulcl  12400  rpdivcl  12402  rpgecl  12405  rphalflt  12406  ge0p1rp  12408  rpneg  12409  negelrp  12410  ltsubrp  12413  ltaddrp  12414  difrp  12415  elrpd  12416  infmrp1  12725  iccdil  12868  icccntr  12870  1mod  13266  expgt0  13458  resqrex  14602  sqrtdiv  14617  sqrtneglem  14618  mulcn2  14944  ef01bndlem  15529  sinltx  15534  met1stc  23128  met2ndci  23129  bcthlem4  23931  itg2mulc  24351  dvferm1  24588  dvne0  24614  reeff1o  25042  ellogdm  25230  cxpge0  25274  cxple2a  25290  cxpcn3lem  25336  cxpaddlelem  25340  cxpaddle  25341  atanbnd  25512  rlimcnp  25551  amgm  25576  chtub  25796  chebbnd1  26056  chto1ub  26060  pntlem3  26193  blocni  28588  dfrp2  30517  rpdp2cl  30584  dp2ltc  30589  dplti  30607  dpgti  30608  dpexpp1  30610  dpmul4  30616  fdvposlt  31980  hgt750lem  32032  unbdqndv2lem2  33962  heiborlem8  35256  2xp3dxp2ge1d  39387  sqrtcvallem1  40331  wallispilem4  42710  perfectALTVlem2  44240  regt1loggt0  44950