Theorem elrp 11710

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

Syntax hints:   ↔ wb 195   ∧ wa 383   ∈ wcel 1977   class class class wbr 4583  ℝcr 9814  0cc0 9815   < clt 9953  ℝ⁺crp 11708

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-br 4584  df-rp 11709

This theorem is referenced by:  elrpii  11711  nnrp  11718  rpgt0  11720  rpregt0  11722  ralrp  11728  rexrp  11729  rpaddcl  11730  rpmulcl  11731  rpdivcl  11732  rpgecl  11735  rphalflt  11736  ge0p1rp  11738  rpneg  11739  negelrp  11740  ltsubrp  11742  ltaddrp  11743  difrp  11744  elrpd  11745  infmrp1  12045  iccdil  12181  icccntr  12183  1mod  12564  expgt0  12755  resqrex  13839  sqrtdiv  13854  sqrtneglem  13855  mulcn2  14174  ef01bndlem  14753  sinltx  14758  met1stc  22136  met2ndci  22137  bcthlem4  22932  itg2mulc  23320  dvferm1  23552  dvne0  23578  reeff1o  24005  ellogdm  24185  cxpge0  24229  cxple2a  24245  cxpcn3lem  24288  cxpaddlelem  24292  cxpaddle  24293  atanbnd  24453  rlimcnp  24492  amgm  24517  chtub  24737  chebbnd1  24961  chto1ub  24965  pntlem3  25098  blocni  27044  dfrp2  28922  unbdqndv2lem2  31671  heiborlem8  32787  wallispilem4  38961  perfectALTVlem2  40165  regt1loggt0  42128