Theorem ressxr 11180

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

Syntax hints:   ∪ cun 3888   ⊆ wss 3890  {cpr 4570  ℝcr 11028  +∞cpnf 11167  -∞cmnf 11168  ℝ^*cxr 11169

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 3432  df-un 3895  df-ss 3907  df-xr 11174

This theorem is referenced by:  rexpssxrxp  11181  rexr  11182  0xr  11183  rexrd  11186  ltrelxr  11197  supxrre  13270  supxrbnd  13271  supxrgtmnf  13272  supxrre1  13273  supxrre2  13274  infxrre  13280  iooval2  13322  fzval2  13455  uzsup  13813  hashxrcl  14310  seqcoll  14417  limsupval2  15433  limsupgre  15434  limsupbnd2  15436  rlimuni  15503  rlimcld2  15531  rlimno1  15607  isercolllem2  15619  isercoll  15621  caucvgrlem  15626  summolem2a  15668  prodmolem2a  15890  ramtlecl  16962  ramxrcl  16979  ismet2  24308  prdsmet  24345  qtopbas  24734  tgqioo  24775  re2ndc  24776  xrsmopn  24788  metdcn2  24815  metdscn2  24833  bndth  24935  ovolunlem1a  25473  ovolunlem1  25474  ovoliunlem1  25479  ovoliun  25482  ovolicc2lem4  25497  voliunlem2  25528  voliunlem3  25529  opnmblALT  25580  vitalilem4  25588  mbfimaopnlem  25632  itg2le  25716  itg2seq  25719  dvfsumrlim  26008  itgsubst  26026  mdegleb  26039  mdeglt  26040  mdegldg  26041  mdegxrcl  26042  mdegcl  26044  mdegaddle  26049  mdegmullem  26053  deg1mul3le  26092  ig1pdvds  26155  aannenlem2  26306  taylfval  26335  radcnvcl  26395  radcnvlt1  26396  radcnvle  26398  xrlimcnp  26945  nmoxr  30852  nmooge0  30853  nmoolb  30857  nmoubi  30858  nmlno0lem  30879  nmopxr  31952  nmfnxr  31965  nmoplb  31993  nmopub  31994  nmfnlb  32010  nmfnleub  32011  nmlnop0iALT  32081  nmopun  32100  branmfn  32191  pjnmopi  32234  xlt2addrd  32847  xreceu  32996  rexdiv  33000  xrsmulgzz  33084  esumcst  34223  icorempo  37681  mblfinlem2  37993  itg2addnc  38009  prdsbnd  38128  rrnequiv  38170  hbtlem2  43570  binomcxplemdvbinom  44798  binomcxplemcvg  44799  binomcxplemnotnn0  44801  suplesup  45787  frexr  45832  zssxr  45844  ssrexr  45878  uzxrd  45908  supminfxr  45910  rpssxr  45926  elicores  45981  ressiocsup  46002  ressioosup  46003  ressiooinf  46005  uzinico  46007  limsupre  46087  limsupresico  46146  limsupmnflem  46166  supcnvlimsup  46186  liminfresico  46217  volicoff  46441  volicofmpt  46443  fourierdlem52  46604  fourierdlem103  46655  fourierdlem104  46656  etransclem48  46728  ioorrnopnlem  46750  fsumlesge0  46823  sge0cl  46827  sge0supre  46835  sge0less  46838  sge0split  46855  sge0seq  46892  volicorescl  46999  ovolval2lem  47089  ovolval5lem2  47099  ovnovollem1  47102  ovnovollem2  47103  iinhoiicclem  47119  iunhoiioolem  47121  iccvonmbllem  47124  vonioolem2  47127  vonioo  47128  vonicclem2  47130  vonicc  47131  pimdecfgtioc  47161  pimincfltioc  47162  pimdecfgtioo  47163  pimincfltioo  47164  smflimsuplem4  47269