Theorem ressxr 11165

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

Syntax hints:   ∪ cun 3896   ⊆ wss 3898  {cpr 4579  ℝcr 11014  +∞cpnf 11152  -∞cmnf 11153  ℝ^*cxr 11154

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-v 3439  df-un 3903  df-ss 3915  df-xr 11159

This theorem is referenced by:  rexpssxrxp  11166  rexr  11167  0xr  11168  rexrd  11171  ltrelxr  11182  supxrre  13230  supxrbnd  13231  supxrgtmnf  13232  supxrre1  13233  supxrre2  13234  infxrre  13240  iooval2  13282  fzval2  13414  uzsup  13771  hashxrcl  14268  seqcoll  14375  limsupval2  15391  limsupgre  15392  limsupbnd2  15394  rlimuni  15461  rlimcld2  15489  rlimno1  15565  isercolllem2  15577  isercoll  15579  caucvgrlem  15584  summolem2a  15626  prodmolem2a  15845  ramtlecl  16916  ramxrcl  16933  ismet2  24251  prdsmet  24288  qtopbas  24677  tgqioo  24718  re2ndc  24719  xrsmopn  24731  metdcn2  24758  metdscn2  24776  bndth  24887  ovolunlem1a  25427  ovolunlem1  25428  ovoliunlem1  25433  ovoliun  25436  ovolicc2lem4  25451  voliunlem2  25482  voliunlem3  25483  opnmblALT  25534  vitalilem4  25542  mbfimaopnlem  25586  itg2le  25670  itg2seq  25673  dvfsumrlim  25968  itgsubst  25986  mdegleb  25999  mdeglt  26000  mdegldg  26001  mdegxrcl  26002  mdegcl  26004  mdegaddle  26009  mdegmullem  26013  deg1mul3le  26052  ig1pdvds  26115  aannenlem2  26267  taylfval  26296  radcnvcl  26356  radcnvlt1  26357  radcnvle  26359  xrlimcnp  26908  nmoxr  30750  nmooge0  30751  nmoolb  30755  nmoubi  30756  nmlno0lem  30777  nmopxr  31850  nmfnxr  31863  nmoplb  31891  nmopub  31892  nmfnlb  31908  nmfnleub  31909  nmlnop0iALT  31979  nmopun  31998  branmfn  32089  pjnmopi  32132  xlt2addrd  32748  xreceu  32911  rexdiv  32915  xrsmulgzz  32999  esumcst  34099  icorempo  37418  mblfinlem2  37721  itg2addnc  37737  prdsbnd  37856  rrnequiv  37898  hbtlem2  43244  binomcxplemdvbinom  44473  binomcxplemcvg  44474  binomcxplemnotnn0  44476  suplesup  45465  frexr  45510  zssxr  45522  ssrexr  45557  uzxrd  45587  supminfxr  45589  rpssxr  45605  elicores  45660  ressiocsup  45681  ressioosup  45682  ressiooinf  45684  uzinico  45686  limsupre  45766  limsupresico  45825  limsupmnflem  45845  supcnvlimsup  45865  liminfresico  45896  volicoff  46120  volicofmpt  46122  fourierdlem52  46283  fourierdlem103  46334  fourierdlem104  46335  etransclem48  46407  ioorrnopnlem  46429  fsumlesge0  46502  sge0cl  46506  sge0supre  46514  sge0less  46517  sge0split  46534  sge0seq  46571  hoicvr  46673  volicorescl  46678  ovolval2lem  46768  ovolval5lem2  46778  ovnovollem1  46781  ovnovollem2  46782  iinhoiicclem  46798  iunhoiioolem  46800  iccvonmbllem  46803  vonioolem2  46806  vonioo  46807  vonicclem2  46809  vonicc  46810  pimdecfgtioc  46840  pimincfltioc  46841  pimdecfgtioo  46842  pimincfltioo  46843  smflimsuplem4  46948