Theorem elrp 11834

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

Syntax hints:   <-> wb 196   /\ wa 384   e. wcel 1990   class class class wbr 4653   RRcr 9935   0cc0 9936   < clt 10074   RR+crp 11832

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-br 4654  df-rp 11833

This theorem is referenced by:  elrpii  11835  nnrp  11842  rpgt0  11844  rpregt0  11846  ralrp  11852  rexrp  11853  rpaddcl  11854  rpmulcl  11855  rpdivcl  11856  rpgecl  11859  rphalflt  11860  ge0p1rp  11862  rpneg  11863  negelrp  11864  ltsubrp  11866  ltaddrp  11867  difrp  11868  elrpd  11869  infmrp1  12174  iccdil  12310  icccntr  12312  1mod  12702  expgt0  12893  resqrex  13991  sqrtdiv  14006  sqrtneglem  14007  mulcn2  14326  ef01bndlem  14914  sinltx  14919  met1stc  22326  met2ndci  22327  bcthlem4  23124  itg2mulc  23514  dvferm1  23748  dvne0  23774  reeff1o  24201  ellogdm  24385  cxpge0  24429  cxple2a  24445  cxpcn3lem  24488  cxpaddlelem  24492  cxpaddle  24493  atanbnd  24653  rlimcnp  24692  amgm  24717  chtub  24937  chebbnd1  25161  chto1ub  25165  pntlem3  25298  blocni  27660  dfrp2  29532  rpdp2cl  29589  dp2ltc  29594  dplti  29613  dpgti  29614  dpexpp1  29616  dpmul4  29622  fdvposlt  30677  hgt750lem  30729  unbdqndv2lem2  32501  heiborlem8  33617  wallispilem4  40285  perfectALTVlem2  41631  regt1loggt0  42330