Theorem elrp 13122

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   ∈ wcel 2144   class class class wbr 5102  ℝcr 11199  0cc0 11200   < clt 11343  ℝ⁺crp 13120

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-br 5103  df-rp 13121

This theorem is used by:  elrpii  13123  nnrp  13132  rpgt0  13133  rpregt0  13135  ralrp  13142  rexrp  13143  rpaddcl  13144  rpmulcl  13145  rpdivcl  13147  rpgecl  13150  rphalflt  13151  ge0p1rp  13153  rpneg  13154  negelrp  13155  ltsubrp  13158  ltaddrp  13159  difrp  13160  elrpd  13161  infmrp1  13475  dfrp2  13525  iccdil  13621  icccntr  13623  1mod  14043  expgt0  14238  resqrex  15417  sqrtdiv  15432  sqrtneglem  15433  mulcn2  15763  ef01bndlem  16352  sinltx  16357  met1stc  24840  met2ndci  24841  bcthlem4  25648  itg2mulc  26068  dvferm1  26305  dvne0  26331  reeff1o  26774  ellogdm  26967  cxpge0  27011  cxple2a  27027  cxpcn3lem  27075  cxpaddlelem  27079  cxpaddle  27080  atanbnd  27254  rlimcnp  27293  amgm  27318  chtub  27539  chebbnd1  27799  chto1ub  27803  pntlem3  27936  blocni  31407  rpdp2cl  33448  dp2ltc  33453  dplti  33471  dpgti  33472  dpexpp1  33474  dpmul4  33480  fdvposlt  35228  hgt750lem  35280  unbdqndv2lem2  37376  heiborlem8  38753  dvrelog2  43115  dvrelog3  43116  sqrtcvallem1  44631  wallispilem4  47078  perfectALTVlem2  48820  regt1loggt0  49648