Theorem ressxr 11302

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 4187	. 2 ⊢ ℝ ⊆ (ℝ ∪ {+∞, -∞})
2		df-xr 11296	. 2 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
3	1, 2	sseqtrri 4032	1 ⊢ ℝ ⊆ ℝ*

Syntax hints:   ∪ cun 3960   ⊆ wss 3962  {cpr 4632  ℝcr 11151  +∞cpnf 11289  -∞cmnf 11290  ℝ^*cxr 11291

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-un 3967  df-ss 3979  df-xr 11296

This theorem is referenced by:  rexpssxrxp  11303  rexr  11304  0xr  11305  rexrd  11308  ltrelxr  11319  supxrre  13365  supxrbnd  13366  supxrgtmnf  13367  supxrre1  13368  supxrre2  13369  infxrre  13374  iooval2  13416  fzval2  13546  uzsup  13899  hashxrcl  14392  seqcoll  14499  limsupval2  15512  limsupgre  15513  limsupbnd2  15515  rlimuni  15582  rlimcld2  15610  rlimno1  15686  isercolllem2  15698  isercoll  15700  caucvgrlem  15705  summolem2a  15747  prodmolem2a  15966  ramtlecl  17033  ramxrcl  17050  ismet2  24358  prdsmet  24395  qtopbas  24795  tgqioo  24835  re2ndc  24836  xrsmopn  24847  metdcn2  24874  metdscn2  24892  bndth  25003  ovolunlem1a  25544  ovolunlem1  25545  ovoliunlem1  25550  ovoliun  25553  ovolicc2lem4  25568  voliunlem2  25599  voliunlem3  25600  opnmblALT  25651  vitalilem4  25659  mbfimaopnlem  25703  itg2le  25788  itg2seq  25791  dvfsumrlim  26086  itgsubst  26104  mdegleb  26117  mdeglt  26118  mdegldg  26119  mdegxrcl  26120  mdegcl  26122  mdegaddle  26127  mdegmullem  26131  deg1mul3le  26170  ig1pdvds  26233  aannenlem2  26385  taylfval  26414  radcnvcl  26474  radcnvlt1  26475  radcnvle  26477  xrlimcnp  27025  nmoxr  30794  nmooge0  30795  nmoolb  30799  nmoubi  30800  nmlno0lem  30821  nmopxr  31894  nmfnxr  31907  nmoplb  31935  nmopub  31936  nmfnlb  31952  nmfnleub  31953  nmlnop0iALT  32023  nmopun  32042  branmfn  32133  pjnmopi  32176  xlt2addrd  32768  xreceu  32888  rexdiv  32892  xrsmulgzz  32993  esumcst  34043  icorempo  37333  mblfinlem2  37644  itg2addnc  37660  prdsbnd  37779  rrnequiv  37821  hbtlem2  43112  binomcxplemdvbinom  44348  binomcxplemcvg  44349  binomcxplemnotnn0  44351  suplesup  45288  frexr  45334  zssxr  45346  ssrexr  45381  uzxrd  45411  supminfxr  45413  rpssxr  45430  elicores  45485  ressiocsup  45506  ressioosup  45507  ressiooinf  45509  uzinico  45512  limsupre  45596  limsupresico  45655  limsupmnflem  45675  supcnvlimsup  45695  liminfresico  45726  volicoff  45950  volicofmpt  45952  fourierdlem52  46113  fourierdlem103  46164  fourierdlem104  46165  etransclem48  46237  ioorrnopnlem  46259  fsumlesge0  46332  sge0cl  46336  sge0supre  46344  sge0less  46347  sge0split  46364  sge0seq  46401  hoicvr  46503  volicorescl  46508  ovolval2lem  46598  ovolval5lem2  46608  ovnovollem1  46611  ovnovollem2  46612  iinhoiicclem  46628  iunhoiioolem  46630  iccvonmbllem  46633  vonioolem2  46636  vonioo  46637  vonicclem2  46639  vonicc  46640  pimdecfgtioc  46670  pimincfltioc  46671  pimdecfgtioo  46672  pimincfltioo  46673  smflimsuplem4  46778