Theorem ressxr 10083

Description: The standard reals are a subset of the extended reals. (Contributed by NM, 14-Oct-2005.)

Assertion

Ref	Expression
ressxr	|- RR C_ RR*

Proof of Theorem ressxr

Step	Hyp	Ref	Expression
1		ssun1 3776	. 2 |- RR C_ ( RR u. { +oo , -oo } )
2		df-xr 10078	. 2 |- RR* = ( RR u. { +oo , -oo } )
3	1, 2	sseqtr4i 3638	1 |- RR C_ RR*

Syntax hints:   u. cun 3572   C_ wss 3574   {cpr 4179   RRcr 9935   +oocpnf 10071   -oocmnf 10072   RR*cxr 10073

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-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-un 3579  df-in 3581  df-ss 3588  df-xr 10078

This theorem is referenced by:  rexpssxrxp  10084  rexr  10085  0xr  10086  rexrd  10089  ltrelxr  10099  supxrre  12157  supxrbnd  12158  supxrgtmnf  12159  supxrre1  12160  supxrre2  12161  infxrre  12166  iooval2  12208  fzval2  12329  uzsup  12662  hashxrcl  13148  seqcoll  13248  limsupval2  14211  limsupgre  14212  limsupbnd2  14214  rlimuni  14281  rlimcld2  14309  rlimno1  14384  isercolllem2  14396  isercoll  14398  caucvgrlem  14403  summolem2a  14446  prodmolem2a  14664  ramtlecl  15704  ramxrcl  15721  ismet2  22138  prdsmet  22175  qtopbas  22563  tgqioo  22603  re2ndc  22604  xrsmopn  22615  metdcn2  22642  metdscn2  22660  bndth  22757  ovolunlem1a  23264  ovolunlem1  23265  ovoliunlem1  23270  ovoliun  23273  ovolicc2lem4  23288  voliunlem2  23319  voliunlem3  23320  opnmblALT  23371  vitalilem4  23380  mbfimaopnlem  23422  itg2le  23506  itg2seq  23509  dvfsumrlim  23794  itgsubst  23812  mdegleb  23824  mdeglt  23825  mdegldg  23826  mdegxrcl  23827  mdegcl  23829  mdegaddle  23834  mdegmullem  23838  deg1mul3le  23876  ig1pdvds  23936  aannenlem2  24084  taylfval  24113  radcnvcl  24171  radcnvlt1  24172  radcnvle  24174  xrlimcnp  24695  nmoxr  27621  nmooge0  27622  nmoolb  27626  nmoubi  27627  nmlno0lem  27648  nmopxr  28725  nmfnxr  28738  nmoplb  28766  nmopub  28767  nmfnlb  28783  nmfnleub  28784  nmlnop0iALT  28854  nmopun  28873  branmfn  28964  pjnmopi  29007  xlt2addrd  29523  xreceu  29630  rexdiv  29634  xrsmulgzz  29678  esumcst  30125  icorempt2  33199  mblfinlem2  33447  itg2addnc  33464  prdsbnd  33592  rrnequiv  33634  hbtlem2  37694  binomcxplemdvbinom  38552  binomcxplemcvg  38553  binomcxplemnotnn0  38555  suplesup  39555  frexr  39604  zssxr  39621  ssrexr  39659  uzxrd  39692  supminfxr  39694  rpssxr  39711  elicores  39760  ressiocsup  39781  ressioosup  39782  ressiooinf  39784  uzinico  39787  limsupre  39873  limsupresico  39932  limsuppnfdlem  39933  limsupmnflem  39952  limsupvaluz2  39970  supcnvlimsup  39972  liminfresico  40003  volicoff  40212  volicofmpt  40214  fourierdlem52  40375  fourierdlem103  40426  fourierdlem104  40427  etransclem48  40499  ioorrnopnlem  40524  fsumlesge0  40594  sge0cl  40598  sge0supre  40606  sge0less  40609  sge0split  40626  sge0seq  40663  hoicvr  40762  volicorescl  40767  ovolval2lem  40857  ovolval5lem2  40867  ovnovollem1  40870  ovnovollem2  40871  iinhoiicclem  40887  iunhoiioolem  40889  iccvonmbllem  40892  vonioolem2  40895  vonioo  40896  vonicclem2  40898  vonicc  40899  pimdecfgtioc  40925  pimincfltioc  40926  pimdecfgtioo  40927  pimincfltioo  40928  smflimsuplem4  41029