Theorem ressxr 11189

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

Syntax hints:   ∪ cun 3887   ⊆ wss 3889  {cpr 4569  ℝcr 11037  +∞cpnf 11176  -∞cmnf 11177  ℝ^*cxr 11178

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 2708

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 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-un 3894  df-ss 3906  df-xr 11183

This theorem is referenced by:  rexpssxrxp  11190  rexr  11191  0xr  11192  rexrd  11195  ltrelxr  11206  supxrre  13279  supxrbnd  13280  supxrgtmnf  13281  supxrre1  13282  supxrre2  13283  infxrre  13289  iooval2  13331  fzval2  13464  uzsup  13822  hashxrcl  14319  seqcoll  14426  limsupval2  15442  limsupgre  15443  limsupbnd2  15445  rlimuni  15512  rlimcld2  15540  rlimno1  15616  isercolllem2  15628  isercoll  15630  caucvgrlem  15635  summolem2a  15677  prodmolem2a  15899  ramtlecl  16971  ramxrcl  16988  ismet2  24298  prdsmet  24335  qtopbas  24724  tgqioo  24765  re2ndc  24766  xrsmopn  24778  metdcn2  24805  metdscn2  24823  bndth  24925  ovolunlem1a  25463  ovolunlem1  25464  ovoliunlem1  25469  ovoliun  25472  ovolicc2lem4  25487  voliunlem2  25518  voliunlem3  25519  opnmblALT  25570  vitalilem4  25578  mbfimaopnlem  25622  itg2le  25706  itg2seq  25709  dvfsumrlim  25998  itgsubst  26016  mdegleb  26029  mdeglt  26030  mdegldg  26031  mdegxrcl  26032  mdegcl  26034  mdegaddle  26039  mdegmullem  26043  deg1mul3le  26082  ig1pdvds  26145  aannenlem2  26295  taylfval  26324  radcnvcl  26382  radcnvlt1  26383  radcnvle  26385  xrlimcnp  26932  nmoxr  30837  nmooge0  30838  nmoolb  30842  nmoubi  30843  nmlno0lem  30864  nmopxr  31937  nmfnxr  31950  nmoplb  31978  nmopub  31979  nmfnlb  31995  nmfnleub  31996  nmlnop0iALT  32066  nmopun  32085  branmfn  32176  pjnmopi  32219  xlt2addrd  32832  xreceu  32981  rexdiv  32985  xrsmulgzz  33069  esumcst  34207  icorempo  37667  mblfinlem2  37979  itg2addnc  37995  prdsbnd  38114  rrnequiv  38156  hbtlem2  43552  binomcxplemdvbinom  44780  binomcxplemcvg  44781  binomcxplemnotnn0  44783  suplesup  45769  frexr  45814  zssxr  45826  ssrexr  45860  uzxrd  45890  supminfxr  45892  rpssxr  45908  elicores  45963  ressiocsup  45984  ressioosup  45985  ressiooinf  45987  uzinico  45989  limsupre  46069  limsupresico  46128  limsupmnflem  46148  supcnvlimsup  46168  liminfresico  46199  volicoff  46423  volicofmpt  46425  fourierdlem52  46586  fourierdlem103  46637  fourierdlem104  46638  etransclem48  46710  ioorrnopnlem  46732  fsumlesge0  46805  sge0cl  46809  sge0supre  46817  sge0less  46820  sge0split  46837  sge0seq  46874  volicorescl  46981  ovolval2lem  47071  ovolval5lem2  47081  ovnovollem1  47084  ovnovollem2  47085  iinhoiicclem  47101  iunhoiioolem  47103  iccvonmbllem  47106  vonioolem2  47109  vonioo  47110  vonicclem2  47112  vonicc  47113  pimdecfgtioc  47143  pimincfltioc  47144  pimdecfgtioo  47145  pimincfltioo  47146  smflimsuplem4  47251