Theorem rexr 9086

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 9085	. 2 |- RR C_ RR*
2	1	sseli 3304	1 |- ( A e. RR -> A e. RR* )

Syntax hints:   -> wi 4   e. wcel 1721   RRcr 8945   RR*cxr 9075

This theorem is referenced by:  rexri  9093  lenlt  9110  ltpnf  10677  mnflt  10678  xrltnsym  10686  xrlttr  10689  xrre  10713  xrre3  10715  max1  10729  max2  10731  min1  10732  min2  10733  maxle  10734  lemin  10735  maxlt  10736  ltmin  10737  max0sub  10738  qbtwnxr  10742  xralrple  10747  alrple  10748  xltnegi  10758  rexadd  10774  xaddnemnf  10776  xaddnepnf  10777  xaddcom  10780  xnegdi  10783  xpncan  10786  xnpcan  10787  xleadd1a  10788  xleadd1  10790  xltadd1  10791  xltadd2  10792  xsubge0  10796  rexmul  10806  xadddilem  10829  xadddir  10831  xrsupsslem  10841  xrinfmsslem  10842  xrub  10846  supxrun  10850  supxrunb1  10854  supxrunb2  10855  supxrbnd1  10856  supxrbnd2  10857  xrsup0  10858  supxrbnd  10863  elioo4g  10927  elioc2  10929  elico2  10930  elicc2  10931  iccss  10934  iooshf  10945  iooneg  10973  icoshft  10975  difreicc  10984  hashbnd  11579  elicc4abs  12078  limsupgord  12221  pcadd  13213  ramubcl  13341  lt6abl  15459  xrsmcmn  16679  xrs1mnd  16691  xrs10  16692  xrsdsreval  16698  psmetge0  18296  xmetge0  18327  imasdsf1olem  18356  bl2in  18383  blssps  18407  blss  18408  blcld  18488  icopnfcld  18755  iocmnfcld  18756  bl2ioo  18776  blssioo  18779  xrtgioo  18790  xrsblre  18795  iccntr  18805  icccmplem2  18807  icccmp  18809  reconnlem2  18811  xrge0tsms  18818  icoopnst  18917  iocopnst  18918  ovolfioo  19317  ovolicc2lem1  19366  ovolicc2lem5  19370  voliunlem3  19399  icombl1  19410  icombl  19411  iccvolcl  19414  ovolioo  19415  uniiccdif  19423  volsup2  19450  mbfimasn  19479  ismbf3d  19499  mbfsup  19509  itg2seq  19587  itg2monolem1  19595  itg2monolem2  19596  itg2monolem3  19597  itg2mono  19598  itg2i1fseqle  19599  itg2i1fseq3  19602  itg2addlem  19603  itg2gt0  19605  itg2cnlem2  19607  dvlip2  19832  ply1remlem  20038  abelthlem3  20302  abelth  20310  sincosq2sgn  20360  sincosq3sgn  20361  sinq12ge0  20369  sincos6thpi  20376  sineq0  20382  efif1olem1  20397  efif1olem2  20398  efif1o  20401  eff1o  20404  loglesqr  20595  basellem1  20816  pntlemo  21254  nmobndi  22229  nmopub2tALT  23365  nmfnleub2  23382  nmopcoadji  23557  rexdiv  24125  xrge0tsmsd  24176  pnfneige0  24289  lmxrge0  24290  hashf2  24427  sxbrsigalem0  24574  orvcgteel  24678  orvclteel  24683  mblfinlem  26143  itg2addnc  26158  itg2gt0cn  26159  iblabsnclem  26167  bddiblnc  26174  areacirclem6  26186  areacirc  26187  ivthALT  26228  blbnd  26386  icodiamlt  26773  ioovolcl  27609

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-v 2918  df-un 3285  df-in 3287  df-ss 3294  df-xr 9080