Theorem ressxr 11188

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

Syntax hints:   ∪ cun 3901   ⊆ wss 3903  {cpr 4584  ℝcr 11037  +∞cpnf 11175  -∞cmnf 11176  ℝ^*cxr 11177

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-un 3908  df-ss 3920  df-xr 11182

This theorem is referenced by:  rexpssxrxp  11189  rexr  11190  0xr  11191  rexrd  11194  ltrelxr  11205  supxrre  13254  supxrbnd  13255  supxrgtmnf  13256  supxrre1  13257  supxrre2  13258  infxrre  13264  iooval2  13306  fzval2  13438  uzsup  13795  hashxrcl  14292  seqcoll  14399  limsupval2  15415  limsupgre  15416  limsupbnd2  15418  rlimuni  15485  rlimcld2  15513  rlimno1  15589  isercolllem2  15601  isercoll  15603  caucvgrlem  15608  summolem2a  15650  prodmolem2a  15869  ramtlecl  16940  ramxrcl  16957  ismet2  24289  prdsmet  24326  qtopbas  24715  tgqioo  24756  re2ndc  24757  xrsmopn  24769  metdcn2  24796  metdscn2  24814  bndth  24925  ovolunlem1a  25465  ovolunlem1  25466  ovoliunlem1  25471  ovoliun  25474  ovolicc2lem4  25489  voliunlem2  25520  voliunlem3  25521  opnmblALT  25572  vitalilem4  25580  mbfimaopnlem  25624  itg2le  25708  itg2seq  25711  dvfsumrlim  26006  itgsubst  26024  mdegleb  26037  mdeglt  26038  mdegldg  26039  mdegxrcl  26040  mdegcl  26042  mdegaddle  26047  mdegmullem  26051  deg1mul3le  26090  ig1pdvds  26153  aannenlem2  26305  taylfval  26334  radcnvcl  26394  radcnvlt1  26395  radcnvle  26397  xrlimcnp  26946  nmoxr  30853  nmooge0  30854  nmoolb  30858  nmoubi  30859  nmlno0lem  30880  nmopxr  31953  nmfnxr  31966  nmoplb  31994  nmopub  31995  nmfnlb  32011  nmfnleub  32012  nmlnop0iALT  32082  nmopun  32101  branmfn  32192  pjnmopi  32235  xlt2addrd  32849  xreceu  33013  rexdiv  33017  xrsmulgzz  33101  esumcst  34240  icorempo  37603  mblfinlem2  37906  itg2addnc  37922  prdsbnd  38041  rrnequiv  38083  hbtlem2  43478  binomcxplemdvbinom  44706  binomcxplemcvg  44707  binomcxplemnotnn0  44709  suplesup  45695  frexr  45740  zssxr  45752  ssrexr  45787  uzxrd  45817  supminfxr  45819  rpssxr  45835  elicores  45890  ressiocsup  45911  ressioosup  45912  ressiooinf  45914  uzinico  45916  limsupre  45996  limsupresico  46055  limsupmnflem  46075  supcnvlimsup  46095  liminfresico  46126  volicoff  46350  volicofmpt  46352  fourierdlem52  46513  fourierdlem103  46564  fourierdlem104  46565  etransclem48  46637  ioorrnopnlem  46659  fsumlesge0  46732  sge0cl  46736  sge0supre  46744  sge0less  46747  sge0split  46764  sge0seq  46801  hoicvr  46903  volicorescl  46908  ovolval2lem  46998  ovolval5lem2  47008  ovnovollem1  47011  ovnovollem2  47012  iinhoiicclem  47028  iunhoiioolem  47030  iccvonmbllem  47033  vonioolem2  47036  vonioo  47037  vonicclem2  47039  vonicc  47040  pimdecfgtioc  47070  pimincfltioc  47071  pimdecfgtioo  47072  pimincfltioo  47073  smflimsuplem4  47178