Theorem elrp 13146

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   ∈ wcel 2147   class class class wbr 5106  ℝcr 11223  0cc0 11224   < clt 11367  ℝ⁺crp 13144

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-br 5107  df-rp 13145

This theorem is used by:  elrpii  13147  nnrp  13156  rpgt0  13157  rpregt0  13159  ralrp  13166  rexrp  13167  rpaddcl  13168  rpmulcl  13169  rpdivcl  13171  rpgecl  13174  rphalflt  13175  ge0p1rp  13177  rpneg  13178  negelrp  13179  ltsubrp  13182  ltaddrp  13183  difrp  13184  elrpd  13185  infmrp1  13499  dfrp2  13549  iccdil  13645  icccntr  13647  1mod  14067  expgt0  14262  resqrex  15443  sqrtdiv  15458  sqrtneglem  15459  mulcn2  15789  ef01bndlem  16378  sinltx  16383  met1stc  24867  met2ndci  24868  bcthlem4  25675  itg2mulc  26095  dvferm1  26332  dvne0  26358  reeff1o  26801  ellogdm  26994  cxpge0  27038  cxple2a  27054  cxpcn3lem  27102  cxpaddlelem  27106  cxpaddle  27107  atanbnd  27281  rlimcnp  27320  amgm  27345  chtub  27566  chebbnd1  27826  chto1ub  27830  pntlem3  27963  blocni  31434  rpdp2cl  33515  dp2ltc  33520  dplti  33538  dpgti  33539  dpexpp1  33541  dpmul4  33547  fdvposlt  35295  hgt750lem  35347  unbdqndv2lem2  37553  heiborlem8  38943  dvrelog2  43305  dvrelog3  43306  sqrtcvallem1  44821  wallispilem4  47281  perfectALTVlem2  49023  regt1loggt0  49851