Theorem elrp 11872

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

Syntax hints:   ↔ wb 196   ∧ wa 383   ∈ wcel 2030   class class class wbr 4685  ℝcr 9973  0cc0 9974   < clt 10112  ℝ⁺crp 11870

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-br 4686  df-rp 11871

This theorem is referenced by:  elrpii  11873  nnrp  11880  rpgt0  11882  rpregt0  11884  ralrp  11890  rexrp  11891  rpaddcl  11892  rpmulcl  11893  rpdivcl  11894  rpgecl  11897  rphalflt  11898  ge0p1rp  11900  rpneg  11901  negelrp  11902  ltsubrp  11904  ltaddrp  11905  difrp  11906  elrpd  11907  infmrp1  12212  iccdil  12348  icccntr  12350  1mod  12742  expgt0  12933  resqrex  14035  sqrtdiv  14050  sqrtneglem  14051  mulcn2  14370  ef01bndlem  14958  sinltx  14963  met1stc  22373  met2ndci  22374  bcthlem4  23170  itg2mulc  23559  dvferm1  23793  dvne0  23819  reeff1o  24246  ellogdm  24430  cxpge0  24474  cxple2a  24490  cxpcn3lem  24533  cxpaddlelem  24537  cxpaddle  24538  atanbnd  24698  rlimcnp  24737  amgm  24762  chtub  24982  chebbnd1  25206  chto1ub  25210  pntlem3  25343  blocni  27788  dfrp2  29660  rpdp2cl  29717  dp2ltc  29722  dplti  29741  dpgti  29742  dpexpp1  29744  dpmul4  29750  fdvposlt  30805  hgt750lem  30857  unbdqndv2lem2  32626  heiborlem8  33747  wallispilem4  40603  perfectALTVlem2  41956  regt1loggt0  42655