Theorem ressxr 11156

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

Syntax hints:   ∪ cun 3900   ⊆ wss 3902  {cpr 4578  ℝcr 11005  +∞cpnf 11143  -∞cmnf 11144  ℝ^*cxr 11145

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 2113  ax-9 2121  ax-ext 2703

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 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-un 3907  df-ss 3919  df-xr 11150

This theorem is referenced by:  rexpssxrxp  11157  rexr  11158  0xr  11159  rexrd  11162  ltrelxr  11173  supxrre  13226  supxrbnd  13227  supxrgtmnf  13228  supxrre1  13229  supxrre2  13230  infxrre  13236  iooval2  13278  fzval2  13410  uzsup  13767  hashxrcl  14264  seqcoll  14371  limsupval2  15387  limsupgre  15388  limsupbnd2  15390  rlimuni  15457  rlimcld2  15485  rlimno1  15561  isercolllem2  15573  isercoll  15575  caucvgrlem  15580  summolem2a  15622  prodmolem2a  15841  ramtlecl  16912  ramxrcl  16929  ismet2  24249  prdsmet  24286  qtopbas  24675  tgqioo  24716  re2ndc  24717  xrsmopn  24729  metdcn2  24756  metdscn2  24774  bndth  24885  ovolunlem1a  25425  ovolunlem1  25426  ovoliunlem1  25431  ovoliun  25434  ovolicc2lem4  25449  voliunlem2  25480  voliunlem3  25481  opnmblALT  25532  vitalilem4  25540  mbfimaopnlem  25584  itg2le  25668  itg2seq  25671  dvfsumrlim  25966  itgsubst  25984  mdegleb  25997  mdeglt  25998  mdegldg  25999  mdegxrcl  26000  mdegcl  26002  mdegaddle  26007  mdegmullem  26011  deg1mul3le  26050  ig1pdvds  26113  aannenlem2  26265  taylfval  26294  radcnvcl  26354  radcnvlt1  26355  radcnvle  26357  xrlimcnp  26906  nmoxr  30744  nmooge0  30745  nmoolb  30749  nmoubi  30750  nmlno0lem  30771  nmopxr  31844  nmfnxr  31857  nmoplb  31885  nmopub  31886  nmfnlb  31902  nmfnleub  31903  nmlnop0iALT  31973  nmopun  31992  branmfn  32083  pjnmopi  32126  xlt2addrd  32740  xreceu  32900  rexdiv  32904  xrsmulgzz  32988  esumcst  34074  icorempo  37391  mblfinlem2  37704  itg2addnc  37720  prdsbnd  37839  rrnequiv  37881  hbtlem2  43163  binomcxplemdvbinom  44392  binomcxplemcvg  44393  binomcxplemnotnn0  44395  suplesup  45384  frexr  45429  zssxr  45441  ssrexr  45476  uzxrd  45506  supminfxr  45508  rpssxr  45524  elicores  45579  ressiocsup  45600  ressioosup  45601  ressiooinf  45603  uzinico  45605  limsupre  45685  limsupresico  45744  limsupmnflem  45764  supcnvlimsup  45784  liminfresico  45815  volicoff  46039  volicofmpt  46041  fourierdlem52  46202  fourierdlem103  46253  fourierdlem104  46254  etransclem48  46326  ioorrnopnlem  46348  fsumlesge0  46421  sge0cl  46425  sge0supre  46433  sge0less  46436  sge0split  46453  sge0seq  46490  hoicvr  46592  volicorescl  46597  ovolval2lem  46687  ovolval5lem2  46697  ovnovollem1  46700  ovnovollem2  46701  iinhoiicclem  46717  iunhoiioolem  46719  iccvonmbllem  46722  vonioolem2  46725  vonioo  46726  vonicclem2  46728  vonicc  46729  pimdecfgtioc  46759  pimincfltioc  46760  pimdecfgtioo  46761  pimincfltioo  46762  smflimsuplem4  46867