Theorem elrp 12953

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 12952	. 2 ⊢ ℝ+ = {𝑥 ∈ ℝ ∣ 0 < 𝑥}
3	1, 2	elrab2 3662	1 ⊢ (𝐴 ∈ ℝ+ ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴))

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2109   class class class wbr 5107  ℝcr 11067  0cc0 11068   < clt 11208  ℝ⁺crp 12951

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108  df-rp 12952

This theorem is referenced by:  elrpii  12954  nnrp  12963  rpgt0  12964  rpregt0  12966  ralrp  12973  rexrp  12974  rpaddcl  12975  rpmulcl  12976  rpdivcl  12978  rpgecl  12981  rphalflt  12982  ge0p1rp  12984  rpneg  12985  negelrp  12986  ltsubrp  12989  ltaddrp  12990  difrp  12991  elrpd  12992  infmrp1  13305  dfrp2  13355  iccdil  13451  icccntr  13453  1mod  13865  expgt0  14060  resqrex  15216  sqrtdiv  15231  sqrtneglem  15232  mulcn2  15562  ef01bndlem  16152  sinltx  16157  met1stc  24409  met2ndci  24410  bcthlem4  25227  itg2mulc  25648  dvferm1  25889  dvne0  25916  reeff1o  26357  ellogdm  26548  cxpge0  26592  cxple2a  26608  cxpcn3lem  26657  cxpaddlelem  26661  cxpaddle  26662  atanbnd  26836  rlimcnp  26875  amgm  26901  chtub  27123  chebbnd1  27383  chto1ub  27387  pntlem3  27520  blocni  30734  rpdp2cl  32802  dp2ltc  32807  dplti  32825  dpgti  32826  dpexpp1  32828  dpmul4  32834  fdvposlt  34590  hgt750lem  34642  unbdqndv2lem2  36498  heiborlem8  37812  dvrelog2  42052  dvrelog3  42053  sqrtcvallem1  43620  wallispilem4  46066  perfectALTVlem2  47723  regt1loggt0  48525