Theorem ressxr 10842

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

Syntax hints:   ∪ cun 3851   ⊆ wss 3853  {cpr 4529  ℝcr 10693  +∞cpnf 10829  -∞cmnf 10830  ℝ^*cxr 10831

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-tru 1546  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-v 3400  df-un 3858  df-in 3860  df-ss 3870  df-xr 10836

This theorem is referenced by:  rexpssxrxp  10843  rexr  10844  0xr  10845  rexrd  10848  ltrelxr  10859  supxrre  12882  supxrbnd  12883  supxrgtmnf  12884  supxrre1  12885  supxrre2  12886  infxrre  12891  iooval2  12933  fzval2  13063  uzsup  13401  hashxrcl  13889  seqcoll  13995  limsupval2  15006  limsupgre  15007  limsupbnd2  15009  rlimuni  15076  rlimcld2  15104  rlimno1  15182  isercolllem2  15194  isercoll  15196  caucvgrlem  15201  summolem2a  15244  prodmolem2a  15459  ramtlecl  16516  ramxrcl  16533  ismet2  23185  prdsmet  23222  qtopbas  23611  tgqioo  23651  re2ndc  23652  xrsmopn  23663  metdcn2  23690  metdscn2  23708  bndth  23809  ovolunlem1a  24347  ovolunlem1  24348  ovoliunlem1  24353  ovoliun  24356  ovolicc2lem4  24371  voliunlem2  24402  voliunlem3  24403  opnmblALT  24454  vitalilem4  24462  mbfimaopnlem  24506  itg2le  24591  itg2seq  24594  dvfsumrlim  24882  itgsubst  24900  mdegleb  24916  mdeglt  24917  mdegldg  24918  mdegxrcl  24919  mdegcl  24921  mdegaddle  24926  mdegmullem  24930  deg1mul3le  24968  ig1pdvds  25028  aannenlem2  25176  taylfval  25205  radcnvcl  25263  radcnvlt1  25264  radcnvle  25266  xrlimcnp  25805  nmoxr  28801  nmooge0  28802  nmoolb  28806  nmoubi  28807  nmlno0lem  28828  nmopxr  29901  nmfnxr  29914  nmoplb  29942  nmopub  29943  nmfnlb  29959  nmfnleub  29960  nmlnop0iALT  30030  nmopun  30049  branmfn  30140  pjnmopi  30183  xlt2addrd  30755  xreceu  30870  rexdiv  30874  xrsmulgzz  30960  esumcst  31697  icorempo  35208  mblfinlem2  35501  itg2addnc  35517  prdsbnd  35637  rrnequiv  35679  hbtlem2  40593  binomcxplemdvbinom  41585  binomcxplemcvg  41586  binomcxplemnotnn0  41588  suplesup  42492  frexr  42538  zssxr  42551  ssrexr  42586  uzxrd  42618  supminfxr  42620  rpssxr  42637  elicores  42687  ressiocsup  42708  ressioosup  42709  ressiooinf  42711  uzinico  42714  limsupre  42800  limsupresico  42859  limsupmnflem  42879  limsupvaluz2  42897  supcnvlimsup  42899  liminfresico  42930  volicoff  43154  volicofmpt  43156  fourierdlem52  43317  fourierdlem103  43368  fourierdlem104  43369  etransclem48  43441  ioorrnopnlem  43463  fsumlesge0  43533  sge0cl  43537  sge0supre  43545  sge0less  43548  sge0split  43565  sge0seq  43602  hoicvr  43704  volicorescl  43709  ovolval2lem  43799  ovolval5lem2  43809  ovnovollem1  43812  ovnovollem2  43813  iinhoiicclem  43829  iunhoiioolem  43831  iccvonmbllem  43834  vonioolem2  43837  vonioo  43838  vonicclem2  43840  vonicc  43841  pimdecfgtioc  43867  pimincfltioc  43868  pimdecfgtioo  43869  pimincfltioo  43870  smflimsuplem4  43971