Theorem elrp 11338

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 4422	. 2 |- ( x = A -> ( 0 < x <-> 0 < A ) )
2		df-rp 11337	. 2 |- RR+ = { x e. RR | 0 < x }
3	1, 2	elrab2 3210	1 |- ( A e. RR+ <-> ( A e. RR /\ 0 < A ) )

Syntax hints:   <-> wb 189   /\ wa 375   e. wcel 1898   class class class wbr 4418   RRcr 9569   0cc0 9570   < clt 9706   RR+crp 11336

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-rab 2758  df-v 3059  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-sn 3981  df-pr 3983  df-op 3987  df-br 4419  df-rp 11337

This theorem is referenced by:  elrpii  11339  nnrp  11345  rpgt0  11347  rpregt0  11349  ralrp  11355  rexrp  11356  rpaddcl  11357  rpmulcl  11358  rpdivcl  11359  rpgecl  11362  rphalflt  11363  ge0p1rp  11365  rpneg  11366  negelrp  11367  ltsubrp  11369  ltaddrp  11370  difrp  11371  elrpd  11372  infmrp1  11668  iccdil  11805  icccntr  11807  1mod  12167  expgt0  12343  resqrex  13369  sqrtdiv  13384  sqrtneglem  13385  mulcn2  13714  ef01bndlem  14293  sinltx  14298  met1stc  21591  met2ndci  21592  bcthlem4  22350  itg2mulc  22761  dvferm1  22993  dvne0  23019  reeff1o  23458  ellogdm  23640  cxpge0  23684  cxple2a  23700  cxpcn3lem  23743  cxpaddlelem  23747  cxpaddle  23748  atanbnd  23908  rlimcnp  23947  amgm  23972  chtub  24196  chebbnd1  24366  chto1ub  24370  pntlem3  24503  blocni  26502  dfrp2  28404  heiborlem8  32196  wallispilem4  38031  perfectALTVlem2  38979  regt1loggt0  40716