Theorem rexr 9685

Description: A standard real is an extended real. (Contributed by NM, 14-Oct-2005.)

Assertion

Ref	Expression
rexr	|- ( A e. RR -> A e. RR* )

Proof of Theorem rexr

Step	Hyp	Ref	Expression
1		ressxr 9683	. 2 |- RR C_ RR*
2	1	sseli 3466	1 |- ( A e. RR -> A e. RR* )

Syntax hints:   -> wi 4   e. wcel 1870   RRcr 9537   RR*cxr 9673

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-v 3089  df-un 3447  df-in 3449  df-ss 3456  df-xr 9678

This theorem is referenced by:  rexri  9692  lenlt  9711  ltpnf  11422  mnflt  11425  xrltnsym  11436  xrlttr  11439  xrre  11464  xrre3  11466  max1  11480  max2  11482  min1  11483  min2  11484  maxle  11485  lemin  11486  maxlt  11487  ltmin  11488  max0sub  11489  qbtwnxr  11493  xralrple  11498  alrple  11499  xltnegi  11509  rexadd  11525  xaddnemnf  11527  xaddnepnf  11528  xaddcom  11531  xnegdi  11534  xpncan  11537  xnpcan  11538  xleadd1a  11539  xleadd1  11541  xltadd1  11542  xltadd2  11543  xsubge0  11547  rexmul  11557  xadddilem  11580  xadddir  11582  xrsupsslem  11592  xrinfmsslem  11593  xrub  11597  supxrun  11601  supxrunb1  11605  supxrunb2  11606  supxrbnd1  11607  supxrbnd2  11608  xrsup0  11609  supxrbnd  11614  infmremnf  11633  elioo4g  11695  elioc2  11697  elico2  11698  elicc2  11699  iccss  11702  iooshf  11713  iooneg  11750  icoshft  11752  difreicc  11762  hashbnd  12518  elicc4abs  13361  limsupgord  13506  pcadd  14797  ramubcl  14939  lt6abl  17464  xrsmcmn  18926  xrs1mnd  18941  xrs10  18942  xrsdsreval  18948  psmetge0  21259  xmetge0  21290  imasdsf1olem  21319  bl2in  21346  blssps  21370  blss  21371  blcld  21451  icopnfcld  21699  iocmnfcld  21700  bl2ioo  21721  blssioo  21724  xrtgioo  21735  xrsblre  21740  iccntr  21750  icccmplem2  21752  icccmp  21754  reconnlem2  21756  xrge0tsms  21763  icoopnst  21863  iocopnst  21864  ovolfioo  22299  ovolicc2lem1  22348  ovolicc2lem5  22352  voliunlem3  22382  icombl1  22393  icombl  22394  iccvolcl  22397  ovolioo  22398  ioovolcl  22399  uniiccdif  22412  volsup2  22440  mbfimasn  22467  ismbf3d  22487  mbfsup  22497  itg2seq  22577  dvlip2  22824  ply1remlem  22988  abelthlem3  23253  abelth  23261  sincosq2sgn  23319  sincosq3sgn  23320  sinq12ge0  23328  sincos6thpi  23335  sineq0  23341  efif1olem1  23356  efif1olem2  23357  efif1o  23360  eff1o  23363  loglesqrt  23563  basellem1  23870  pntlemo  24308  nmobndi  26261  nmopub2tALT  27397  nmfnleub2  27414  nmopcoadji  27589  rexdiv  28233  xrge0tsmsd  28387  pnfneige0  28596  lmxrge0  28597  hashf2  28744  sxbrsigalem0  28932  omssubadd  28961  orvcgteel  29126  orvclteel  29131  sgnclre  29198  sgnneg  29199  signstfvneq0  29249  ivthALT  30776  icorempt2  31488  icoreunrn  31496  iooelexlt  31499  relowlssretop  31500  relowlpssretop  31501  poimir  31677  mblfinlem2  31682  iblabsnclem  31709  bddiblnc  31716  ftc1anclem1  31721  ftc1anclem6  31726  areacirclem5  31740  areacirc  31741  blbnd  31823  icodiamlt  35374  iocmbl  35796  supxrre3  37157  supxrgere  37165  ioomidp  37200  limsupre  37293  limsupreOLD  37294  icccncfext  37337  volioc  37418  fourierdlem113  37651  bgoldbtbndlem3  38292