Theorem elrp 11213

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

Syntax hints:   <-> wb 184   /\ wa 369   e. wcel 1762   class class class wbr 4442   RRcr 9482   0cc0 9483   < clt 9619   RR+crp 11211

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1963  ax-ext 2440

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2612  df-rab 2818  df-v 3110  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-nul 3781  df-if 3935  df-sn 4023  df-pr 4025  df-op 4029  df-br 4443  df-rp 11212

This theorem is referenced by:  elrpii  11214  nnrp  11220  rpgt0  11222  rpregt0  11224  ralrp  11229  rexrp  11230  rpaddcl  11231  rpmulcl  11232  rpdivcl  11233  rpgecl  11236  rphalflt  11237  ge0p1rp  11239  rpneg  11240  ltsubrp  11242  ltaddrp  11243  difrp  11244  elrpd  11245  iccdil  11649  icccntr  11651  1mod  11986  expgt0  12156  resqrex  13036  sqrdiv  13051  sqrneglem  13052  mulcn2  13369  ef01bndlem  13771  sinltx  13776  met1stc  20754  met2ndci  20755  bcthlem4  21496  itg2mulc  21884  dvferm1  22116  dvne0  22142  reeff1o  22571  ellogdm  22743  cxpge0  22787  cxple2a  22803  cxpcn3lem  22844  cxpaddlelem  22848  cxpaddle  22849  atanbnd  22980  rlimcnp  23018  amgm  23043  chtub  23210  chebbnd1  23380  chto1ub  23384  pntlem3  23517  blocni  25384  negelrp  27220  heiborlem8  29906  limclner  31150  pirp2  31157  wallispilem4  31325  dirkerper  31353  dirkercncflem2  31361  fourierdlem4  31368  fourierdlem42  31406  fourierdlem43  31407  fourierdlem77  31441  fourierswlem  31488  fouriersw  31489