Theorem elrp 11251

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

Assertion

Ref	Expression
elrp

Proof of Theorem elrp

Dummy variable is distinct from all other variables.

Step	Hyp	Ref	Expression
1		breq2 4456	. 2
2		df-rp 11250	. 2
3	1, 2	elrab2 3259	1

Syntax hints:  <->wb 184  /\wa 369  e.wcel 1818   class class class wbr 4452  cr 9512  0cc0 9513  clt 9649  crp 11249

This theorem is referenced by:  elrpii  11252  nnrp  11258  rpgt0  11260  rpregt0  11262  ralrp  11267  rexrp  11268  rpaddcl  11269  rpmulcl  11270  rpdivcl  11271  rpgecl  11274  rphalflt  11275  ge0p1rp  11277  rpneg  11278  ltsubrp  11280  ltaddrp  11281  difrp  11282  elrpd  11283  iccdil  11687  icccntr  11689  1mod  12028  expgt0  12199  resqrex  13084  sqrtdiv  13099  sqrtneglem  13100  mulcn2  13418  ef01bndlem  13919  sinltx  13924  met1stc  21024  met2ndci  21025  bcthlem4  21766  itg2mulc  22154  dvferm1  22386  dvne0  22412  reeff1o  22842  ellogdm  23020  cxpge0  23064  cxple2a  23080  cxpcn3lem  23121  cxpaddlelem  23125  cxpaddle  23126  atanbnd  23257  rlimcnp  23295  amgm  23320  chtub  23487  chebbnd1  23657  chto1ub  23661  pntlem3  23794  blocni  25720  negelrp  27564  heiborlem8  30314  wallispilem4  31850

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-br 4453  df-rp 11250