Theorem elrp 12973

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

Syntax hints:   ↔ wb 205   ∧ wa 395   ∈ wcel 2098   class class class wbr 5138  ℝcr 11105  0cc0 11106   < clt 11245  ℝ⁺crp 12971

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2695

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-rab 3425  df-v 3468  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-nul 4315  df-if 4521  df-sn 4621  df-pr 4623  df-op 4627  df-br 5139  df-rp 12972

This theorem is referenced by:  elrpii  12974  nnrp  12982  rpgt0  12983  rpregt0  12985  ralrp  12991  rexrp  12992  rpaddcl  12993  rpmulcl  12994  rpdivcl  12996  rpgecl  12999  rphalflt  13000  ge0p1rp  13002  rpneg  13003  negelrp  13004  ltsubrp  13007  ltaddrp  13008  difrp  13009  elrpd  13010  infmrp1  13320  dfrp2  13370  iccdil  13464  icccntr  13466  1mod  13865  expgt0  14058  resqrex  15194  sqrtdiv  15209  sqrtneglem  15210  mulcn2  15537  ef01bndlem  16124  sinltx  16129  met1stc  24352  met2ndci  24353  bcthlem4  25177  itg2mulc  25599  dvferm1  25839  dvne0  25866  reeff1o  26301  ellogdm  26489  cxpge0  26533  cxple2a  26549  cxpcn3lem  26598  cxpaddlelem  26602  cxpaddle  26603  atanbnd  26774  rlimcnp  26813  amgm  26839  chtub  27061  chebbnd1  27321  chto1ub  27325  pntlem3  27458  blocni  30527  rpdp2cl  32515  dp2ltc  32520  dplti  32538  dpgti  32539  dpexpp1  32541  dpmul4  32547  fdvposlt  34100  hgt750lem  34152  unbdqndv2lem2  35876  heiborlem8  37176  dvrelog2  41422  dvrelog3  41423  2xp3dxp2ge1d  41515  sqrtcvallem1  42871  wallispilem4  45269  perfectALTVlem2  46875  regt1loggt0  47410