Theorem elrp 11266

Description: Membership in the set of positive reals. (Contributed by NM, 27-Oct-2007.)

Assertion

Ref	Expression
elrp	|- ( A e. RR+ <-> ( A e. RR /\ 0 < A ) )

Proof of Theorem elrp

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		breq2 4398	. 2 |- ( x = A -> ( 0 < x <-> 0 < A ) )
2		df-rp 11265	. 2 |- RR+ = { x e. RR | 0 < x }
3	1, 2	elrab2 3208	1 |- ( A e. RR+ <-> ( A e. RR /\ 0 < A ) )

Syntax hints:   <-> wb 184   /\ wa 367   e. wcel 1842   class class class wbr 4394   RRcr 9520   0cc0 9521   < clt 9657   RR+crp 11264

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-rab 2762  df-v 3060  df-dif 3416  df-un 3418  df-in 3420  df-ss 3427  df-nul 3738  df-if 3885  df-sn 3972  df-pr 3974  df-op 3978  df-br 4395  df-rp 11265

This theorem is referenced by:  elrpii  11267  nnrp  11273  rpgt0  11275  rpregt0  11277  ralrp  11283  rexrp  11284  rpaddcl  11285  rpmulcl  11286  rpdivcl  11287  rpgecl  11290  rphalflt  11291  ge0p1rp  11293  rpneg  11294  negelrp  11295  ltsubrp  11297  ltaddrp  11298  difrp  11299  elrpd  11300  iccdil  11710  icccntr  11712  1mod  12065  expgt0  12241  resqrex  13231  sqrtdiv  13246  sqrtneglem  13247  mulcn2  13565  ef01bndlem  14126  sinltx  14131  met1stc  21314  met2ndci  21315  bcthlem4  22056  itg2mulc  22444  dvferm1  22676  dvne0  22702  reeff1o  23132  ellogdm  23312  cxpge0  23356  cxple2a  23372  cxpcn3lem  23415  cxpaddlelem  23419  cxpaddle  23420  atanbnd  23580  rlimcnp  23619  amgm  23644  chtub  23866  chebbnd1  24036  chto1ub  24040  pntlem3  24173  blocni  26120  dfrp2  28015  heiborlem8  31576  wallispilem4  37199  perfectALTVlem2  37778  regt1loggt0  38648