Theorem ressxr 11225

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

Assertion

Ref	Expression
ressxr	⊢ ℝ ⊆ ℝ*

Proof of Theorem ressxr

Step	Hyp	Ref	Expression
1		ssun1 4144	. 2 ⊢ ℝ ⊆ (ℝ ∪ {+∞, -∞})
2		df-xr 11219	. 2 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
3	1, 2	sseqtrri 3999	1 ⊢ ℝ ⊆ ℝ*

Syntax hints:   ∪ cun 3915   ⊆ wss 3917  {cpr 4594  ℝcr 11074  +∞cpnf 11212  -∞cmnf 11213  ℝ^*cxr 11214

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-un 3922  df-ss 3934  df-xr 11219

This theorem is referenced by:  rexpssxrxp  11226  rexr  11227  0xr  11228  rexrd  11231  ltrelxr  11242  supxrre  13294  supxrbnd  13295  supxrgtmnf  13296  supxrre1  13297  supxrre2  13298  infxrre  13304  iooval2  13346  fzval2  13478  uzsup  13832  hashxrcl  14329  seqcoll  14436  limsupval2  15453  limsupgre  15454  limsupbnd2  15456  rlimuni  15523  rlimcld2  15551  rlimno1  15627  isercolllem2  15639  isercoll  15641  caucvgrlem  15646  summolem2a  15688  prodmolem2a  15907  ramtlecl  16978  ramxrcl  16995  ismet2  24228  prdsmet  24265  qtopbas  24654  tgqioo  24695  re2ndc  24696  xrsmopn  24708  metdcn2  24735  metdscn2  24753  bndth  24864  ovolunlem1a  25404  ovolunlem1  25405  ovoliunlem1  25410  ovoliun  25413  ovolicc2lem4  25428  voliunlem2  25459  voliunlem3  25460  opnmblALT  25511  vitalilem4  25519  mbfimaopnlem  25563  itg2le  25647  itg2seq  25650  dvfsumrlim  25945  itgsubst  25963  mdegleb  25976  mdeglt  25977  mdegldg  25978  mdegxrcl  25979  mdegcl  25981  mdegaddle  25986  mdegmullem  25990  deg1mul3le  26029  ig1pdvds  26092  aannenlem2  26244  taylfval  26273  radcnvcl  26333  radcnvlt1  26334  radcnvle  26336  xrlimcnp  26885  nmoxr  30702  nmooge0  30703  nmoolb  30707  nmoubi  30708  nmlno0lem  30729  nmopxr  31802  nmfnxr  31815  nmoplb  31843  nmopub  31844  nmfnlb  31860  nmfnleub  31861  nmlnop0iALT  31931  nmopun  31950  branmfn  32041  pjnmopi  32084  xlt2addrd  32689  xreceu  32849  rexdiv  32853  xrsmulgzz  32954  esumcst  34060  icorempo  37346  mblfinlem2  37659  itg2addnc  37675  prdsbnd  37794  rrnequiv  37836  hbtlem2  43120  binomcxplemdvbinom  44349  binomcxplemcvg  44350  binomcxplemnotnn0  44352  suplesup  45342  frexr  45388  zssxr  45400  ssrexr  45435  uzxrd  45465  supminfxr  45467  rpssxr  45483  elicores  45538  ressiocsup  45559  ressioosup  45560  ressiooinf  45562  uzinico  45564  limsupre  45646  limsupresico  45705  limsupmnflem  45725  supcnvlimsup  45745  liminfresico  45776  volicoff  46000  volicofmpt  46002  fourierdlem52  46163  fourierdlem103  46214  fourierdlem104  46215  etransclem48  46287  ioorrnopnlem  46309  fsumlesge0  46382  sge0cl  46386  sge0supre  46394  sge0less  46397  sge0split  46414  sge0seq  46451  hoicvr  46553  volicorescl  46558  ovolval2lem  46648  ovolval5lem2  46658  ovnovollem1  46661  ovnovollem2  46662  iinhoiicclem  46678  iunhoiioolem  46680  iccvonmbllem  46683  vonioolem2  46686  vonioo  46687  vonicclem2  46689  vonicc  46690  pimdecfgtioc  46720  pimincfltioc  46721  pimdecfgtioo  46722  pimincfltioo  46723  smflimsuplem4  46828