Theorem elrp 12038

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

Syntax hints:   ↔ wb 196   ∧ wa 382   ∈ wcel 2145   class class class wbr 4787  ℝcr 10138  0cc0 10139   < clt 10277  ℝ⁺crp 12036

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 829  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-rab 3070  df-v 3353  df-dif 3727  df-un 3729  df-in 3731  df-ss 3738  df-nul 4065  df-if 4227  df-sn 4318  df-pr 4320  df-op 4324  df-br 4788  df-rp 12037

This theorem is referenced by:  elrpii  12039  nnrp  12046  rpgt0  12048  rpregt0  12050  ralrp  12056  rexrp  12057  rpaddcl  12058  rpmulcl  12059  rpdivcl  12060  rpgecl  12063  rphalflt  12064  ge0p1rp  12066  rpneg  12067  negelrp  12068  ltsubrp  12070  ltaddrp  12071  difrp  12072  elrpd  12073  infmrp1  12380  iccdil  12518  icccntr  12520  1mod  12911  expgt0  13101  resqrex  14200  sqrtdiv  14215  sqrtneglem  14216  mulcn2  14535  ef01bndlem  15121  sinltx  15126  met1stc  22547  met2ndci  22548  bcthlem4  23344  itg2mulc  23735  dvferm1  23969  dvne0  23995  reeff1o  24422  ellogdm  24607  cxpge0  24651  cxple2a  24667  cxpcn3lem  24710  cxpaddlelem  24714  cxpaddle  24715  atanbnd  24875  rlimcnp  24914  amgm  24939  chtub  25159  chebbnd1  25383  chto1ub  25387  pntlem3  25520  blocni  28001  dfrp2  29873  rpdp2cl  29930  dp2ltc  29935  dplti  29954  dpgti  29955  dpexpp1  29957  dpmul4  29963  fdvposlt  31018  hgt750lem  31070  unbdqndv2lem2  32839  heiborlem8  33950  wallispilem4  40803  perfectALTVlem2  42160  regt1loggt0  42859