Theorem elrp 13077

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   ∈ wcel 2145   class class class wbr 5103  ℝcr 11156  0cc0 11157   < clt 11300  ℝ⁺crp 13075

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-rp 13076

This theorem is used by:  elrpii  13078  nnrp  13087  rpgt0  13088  rpregt0  13090  ralrp  13097  rexrp  13098  rpaddcl  13099  rpmulcl  13100  rpdivcl  13102  rpgecl  13105  rphalflt  13106  ge0p1rp  13108  rpneg  13109  negelrp  13110  ltsubrp  13113  ltaddrp  13114  difrp  13115  elrpd  13116  infmrp1  13430  dfrp2  13480  iccdil  13576  icccntr  13578  1mod  13997  expgt0  14192  resqrex  15370  sqrtdiv  15385  sqrtneglem  15386  mulcn2  15716  ef01bndlem  16305  sinltx  16310  met1stc  24787  met2ndci  24788  bcthlem4  25595  itg2mulc  26015  dvferm1  26252  dvne0  26278  reeff1o  26723  ellogdm  26916  cxpge0  26960  cxple2a  26976  cxpcn3lem  27024  cxpaddlelem  27028  cxpaddle  27029  atanbnd  27203  rlimcnp  27242  amgm  27267  chtub  27488  chebbnd1  27748  chto1ub  27752  pntlem3  27885  blocni  31326  rpdp2cl  33367  dp2ltc  33372  dplti  33390  dpgti  33391  dpexpp1  33393  dpmul4  33399  fdvposlt  35148  hgt750lem  35200  unbdqndv2lem2  37292  heiborlem8  38666  dvrelog2  43028  dvrelog3  43029  sqrtcvallem1  44569  wallispilem4  46994  perfectALTVlem2  48736  regt1loggt0  49564