Theorem ressxr 11258

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

Syntax hints:   ∪ cun 3947   ⊆ wss 3949  {cpr 4631  ℝcr 11109  +∞cpnf 11245  -∞cmnf 11246  ℝ^*cxr 11247

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-un 3954  df-in 3956  df-ss 3966  df-xr 11252

This theorem is referenced by:  rexpssxrxp  11259  rexr  11260  0xr  11261  rexrd  11264  ltrelxr  11275  supxrre  13306  supxrbnd  13307  supxrgtmnf  13308  supxrre1  13309  supxrre2  13310  infxrre  13315  iooval2  13357  fzval2  13487  uzsup  13828  hashxrcl  14317  seqcoll  14425  limsupval2  15424  limsupgre  15425  limsupbnd2  15427  rlimuni  15494  rlimcld2  15522  rlimno1  15600  isercolllem2  15612  isercoll  15614  caucvgrlem  15619  summolem2a  15661  prodmolem2a  15878  ramtlecl  16933  ramxrcl  16950  ismet2  23839  prdsmet  23876  qtopbas  24276  tgqioo  24316  re2ndc  24317  xrsmopn  24328  metdcn2  24355  metdscn2  24373  bndth  24474  ovolunlem1a  25013  ovolunlem1  25014  ovoliunlem1  25019  ovoliun  25022  ovolicc2lem4  25037  voliunlem2  25068  voliunlem3  25069  opnmblALT  25120  vitalilem4  25128  mbfimaopnlem  25172  itg2le  25257  itg2seq  25260  dvfsumrlim  25548  itgsubst  25566  mdegleb  25582  mdeglt  25583  mdegldg  25584  mdegxrcl  25585  mdegcl  25587  mdegaddle  25592  mdegmullem  25596  deg1mul3le  25634  ig1pdvds  25694  aannenlem2  25842  taylfval  25871  radcnvcl  25929  radcnvlt1  25930  radcnvle  25932  xrlimcnp  26473  nmoxr  30050  nmooge0  30051  nmoolb  30055  nmoubi  30056  nmlno0lem  30077  nmopxr  31150  nmfnxr  31163  nmoplb  31191  nmopub  31192  nmfnlb  31208  nmfnleub  31209  nmlnop0iALT  31279  nmopun  31298  branmfn  31389  pjnmopi  31432  xlt2addrd  32002  xreceu  32119  rexdiv  32123  xrsmulgzz  32210  esumcst  33092  icorempo  36280  mblfinlem2  36574  itg2addnc  36590  prdsbnd  36709  rrnequiv  36751  hbtlem2  41914  binomcxplemdvbinom  43160  binomcxplemcvg  43161  binomcxplemnotnn0  43163  suplesup  44097  frexr  44143  zssxr  44155  ssrexr  44190  uzxrd  44220  supminfxr  44222  rpssxr  44239  elicores  44294  ressiocsup  44315  ressioosup  44316  ressiooinf  44318  uzinico  44321  limsupre  44405  limsupresico  44464  limsupmnflem  44484  limsupvaluz2  44502  supcnvlimsup  44504  liminfresico  44535  volicoff  44759  volicofmpt  44761  fourierdlem52  44922  fourierdlem103  44973  fourierdlem104  44974  etransclem48  45046  ioorrnopnlem  45068  fsumlesge0  45141  sge0cl  45145  sge0supre  45153  sge0less  45156  sge0split  45173  sge0seq  45210  hoicvr  45312  volicorescl  45317  ovolval2lem  45407  ovolval5lem2  45417  ovnovollem1  45420  ovnovollem2  45421  iinhoiicclem  45437  iunhoiioolem  45439  iccvonmbllem  45442  vonioolem2  45445  vonioo  45446  vonicclem2  45448  vonicc  45449  pimdecfgtioc  45479  pimincfltioc  45480  pimdecfgtioo  45481  pimincfltioo  45482  smflimsuplem4  45587