Theorem elrp 12921

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2114   class class class wbr 5100  ℝcr 11039  0cc0 11040   < clt 11180  ℝ⁺crp 12919

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-rp 12920

This theorem is referenced by:  elrpii  12922  nnrp  12931  rpgt0  12932  rpregt0  12934  ralrp  12941  rexrp  12942  rpaddcl  12943  rpmulcl  12944  rpdivcl  12946  rpgecl  12949  rphalflt  12950  ge0p1rp  12952  rpneg  12953  negelrp  12954  ltsubrp  12957  ltaddrp  12958  difrp  12959  elrpd  12960  infmrp1  13274  dfrp2  13324  iccdil  13420  icccntr  13422  1mod  13837  expgt0  14032  resqrex  15187  sqrtdiv  15202  sqrtneglem  15203  mulcn2  15533  ef01bndlem  16123  sinltx  16128  met1stc  24482  met2ndci  24483  bcthlem4  25300  itg2mulc  25721  dvferm1  25962  dvne0  25989  reeff1o  26430  ellogdm  26621  cxpge0  26665  cxple2a  26681  cxpcn3lem  26730  cxpaddlelem  26734  cxpaddle  26735  atanbnd  26909  rlimcnp  26948  amgm  26974  chtub  27196  chebbnd1  27456  chto1ub  27460  pntlem3  27593  blocni  30899  rpdp2cl  32980  dp2ltc  32985  dplti  33003  dpgti  33004  dpexpp1  33006  dpmul4  33012  fdvposlt  34783  hgt750lem  34835  unbdqndv2lem2  36738  heiborlem8  38098  dvrelog2  42463  dvrelog3  42464  sqrtcvallem1  44016  wallispilem4  46455  perfectALTVlem2  48111  regt1loggt0  48925