Theorem ressxr 11178

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

Syntax hints:   ∪ cun 3903   ⊆ wss 3905  {cpr 4581  ℝcr 11027  +∞cpnf 11165  -∞cmnf 11166  ℝ^*cxr 11167

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 2701

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 2708  df-cleq 2721  df-clel 2803  df-v 3440  df-un 3910  df-ss 3922  df-xr 11172

This theorem is referenced by:  rexpssxrxp  11179  rexr  11180  0xr  11181  rexrd  11184  ltrelxr  11195  supxrre  13247  supxrbnd  13248  supxrgtmnf  13249  supxrre1  13250  supxrre2  13251  infxrre  13257  iooval2  13299  fzval2  13431  uzsup  13785  hashxrcl  14282  seqcoll  14389  limsupval2  15405  limsupgre  15406  limsupbnd2  15408  rlimuni  15475  rlimcld2  15503  rlimno1  15579  isercolllem2  15591  isercoll  15593  caucvgrlem  15598  summolem2a  15640  prodmolem2a  15859  ramtlecl  16930  ramxrcl  16947  ismet2  24237  prdsmet  24274  qtopbas  24663  tgqioo  24704  re2ndc  24705  xrsmopn  24717  metdcn2  24744  metdscn2  24762  bndth  24873  ovolunlem1a  25413  ovolunlem1  25414  ovoliunlem1  25419  ovoliun  25422  ovolicc2lem4  25437  voliunlem2  25468  voliunlem3  25469  opnmblALT  25520  vitalilem4  25528  mbfimaopnlem  25572  itg2le  25656  itg2seq  25659  dvfsumrlim  25954  itgsubst  25972  mdegleb  25985  mdeglt  25986  mdegldg  25987  mdegxrcl  25988  mdegcl  25990  mdegaddle  25995  mdegmullem  25999  deg1mul3le  26038  ig1pdvds  26101  aannenlem2  26253  taylfval  26282  radcnvcl  26342  radcnvlt1  26343  radcnvle  26345  xrlimcnp  26894  nmoxr  30728  nmooge0  30729  nmoolb  30733  nmoubi  30734  nmlno0lem  30755  nmopxr  31828  nmfnxr  31841  nmoplb  31869  nmopub  31870  nmfnlb  31886  nmfnleub  31887  nmlnop0iALT  31957  nmopun  31976  branmfn  32067  pjnmopi  32110  xlt2addrd  32715  xreceu  32875  rexdiv  32879  xrsmulgzz  32976  esumcst  34032  icorempo  37327  mblfinlem2  37640  itg2addnc  37656  prdsbnd  37775  rrnequiv  37817  hbtlem2  43100  binomcxplemdvbinom  44329  binomcxplemcvg  44330  binomcxplemnotnn0  44332  suplesup  45322  frexr  45368  zssxr  45380  ssrexr  45415  uzxrd  45445  supminfxr  45447  rpssxr  45463  elicores  45518  ressiocsup  45539  ressioosup  45540  ressiooinf  45542  uzinico  45544  limsupre  45626  limsupresico  45685  limsupmnflem  45705  supcnvlimsup  45725  liminfresico  45756  volicoff  45980  volicofmpt  45982  fourierdlem52  46143  fourierdlem103  46194  fourierdlem104  46195  etransclem48  46267  ioorrnopnlem  46289  fsumlesge0  46362  sge0cl  46366  sge0supre  46374  sge0less  46377  sge0split  46394  sge0seq  46431  hoicvr  46533  volicorescl  46538  ovolval2lem  46628  ovolval5lem2  46638  ovnovollem1  46641  ovnovollem2  46642  iinhoiicclem  46658  iunhoiioolem  46660  iccvonmbllem  46663  vonioolem2  46666  vonioo  46667  vonicclem2  46669  vonicc  46670  pimdecfgtioc  46700  pimincfltioc  46701  pimdecfgtioo  46702  pimincfltioo  46703  smflimsuplem4  46808