Theorem ressxr 11187

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

Syntax hints:   ∪ cun 3888   ⊆ wss 3890  {cpr 4564  ℝcr 11035  +∞cpnf 11174  -∞cmnf 11175  ℝ^*cxr 11176

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-v 3434  df-un 3895  df-ss 3907  df-xr 11181

This theorem is referenced by:  rexpssxrxp  11188  rexr  11189  0xr  11190  rexrd  11193  ltrelxr  11204  supxrre  13277  supxrbnd  13278  supxrgtmnf  13279  supxrre1  13280  supxrre2  13281  infxrre  13287  iooval2  13329  fzval2  13462  uzsup  13820  hashxrcl  14317  seqcoll  14424  limsupval2  15440  limsupgre  15441  limsupbnd2  15443  rlimuni  15510  rlimcld2  15538  rlimno1  15614  isercolllem2  15626  isercoll  15628  caucvgrlem  15633  summolem2a  15675  prodmolem2a  15897  ramtlecl  16969  ramxrcl  16986  ismet2  24323  prdsmet  24360  qtopbas  24749  tgqioo  24790  re2ndc  24791  xrsmopn  24803  metdcn2  24830  metdscn2  24848  bndth  24950  ovolunlem1a  25488  ovolunlem1  25489  ovoliunlem1  25494  ovoliun  25497  ovolicc2lem4  25512  voliunlem2  25543  voliunlem3  25544  opnmblALT  25595  vitalilem4  25603  mbfimaopnlem  25647  itg2le  25731  itg2seq  25734  dvfsumrlim  26023  itgsubst  26041  mdegleb  26054  mdeglt  26055  mdegldg  26056  mdegxrcl  26057  mdegcl  26059  mdegaddle  26064  mdegmullem  26068  deg1mul3le  26107  ig1pdvds  26170  aannenlem2  26320  taylfval  26349  radcnvcl  26407  radcnvlt1  26408  radcnvle  26410  xrlimcnp  26957  nmoxr  30862  nmooge0  30863  nmoolb  30867  nmoubi  30868  nmlno0lem  30889  nmopxr  31962  nmfnxr  31975  nmoplb  32003  nmopub  32004  nmfnlb  32020  nmfnleub  32021  nmlnop0iALT  32091  nmopun  32110  branmfn  32201  pjnmopi  32244  xlt2addrd  32858  xreceu  33007  rexdiv  33011  xrsmulgzz  33095  esumcst  34254  icorempo  37720  mblfinlem2  38032  itg2addnc  38048  prdsbnd  38167  rrnequiv  38209  hbtlem2  43576  binomcxplemdvbinom  44804  binomcxplemcvg  44805  binomcxplemnotnn0  44807  suplesup  45791  frexr  45836  zssxr  45848  ssrexr  45882  uzxrd  45912  supminfxr  45914  rpssxr  45930  elicores  45985  ressiocsup  46006  ressioosup  46007  ressiooinf  46009  uzinico  46011  limsupre  46091  limsupresico  46150  limsupmnflem  46170  supcnvlimsup  46190  liminfresico  46221  volicoff  46445  volicofmpt  46447  fourierdlem52  46608  fourierdlem103  46659  fourierdlem104  46660  etransclem48  46732  ioorrnopnlem  46754  fsumlesge0  46827  sge0cl  46831  sge0supre  46839  sge0less  46842  sge0split  46859  sge0seq  46896  volicorescl  47003  ovolval2lem  47093  ovolval5lem2  47103  ovnovollem1  47106  ovnovollem2  47107  iinhoiicclem  47123  iunhoiioolem  47125  iccvonmbllem  47128  vonioolem2  47131  vonioo  47132  vonicclem2  47134  vonicc  47135  pimdecfgtioc  47165  pimincfltioc  47166  pimdecfgtioo  47167  pimincfltioo  47168  smflimsuplem4  47273