Theorem ressxr 11280

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

This proof depends on syntax axioms:   ∪ cun 3900   ⊆ wss 3902  {cpr 4589  ℝcr 11126  +∞cpnf 11267  -∞cmnf 11268  ℝ^*cxr 11269

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3455  df-un 3907  df-ss 3919  df-xr 11274

This theorem is used by:  rexpssxrxp  11281  rexr  11282  0xr  11283  rexrd  11286  ltrelxr  11297  supxrre  13381  supxrbnd  13382  supxrgtmnf  13383  supxrre1  13384  supxrre2  13385  infxrre  13391  iooval2  13433  fzval2  13566  uzsup  13926  hashxrcl  14423  seqcoll  14531  limsupval2  15569  limsupgre  15570  limsupbnd2  15572  rlimuni  15639  rlimcld2  15667  rlimno1  15743  isercolllem2  15755  isercoll  15757  caucvgrlem  15762  summolem2a  15803  prodmolem2a  16025  ramtlecl  17096  ramxrcl  17113  ismet2  24560  prdsmet  24597  qtopbas  24986  tgqioo  25027  re2ndc  25028  xrsmopn  25040  metdcn2  25067  metdscn2  25085  bndth  25187  ovolunlem1a  25725  ovolunlem1  25726  ovoliunlem1  25731  ovoliun  25734  ovolicc2lem4  25749  voliunlem2  25780  voliunlem3  25781  opnmblALT  25832  vitalilem4  25840  mbfimaopnlem  25884  itg2le  25968  itg2seq  25971  dvfsumrlim  26260  itgsubst  26278  mdegleb  26291  mdeglt  26292  mdegldg  26293  mdegxrcl  26294  mdegcl  26296  mdegaddle  26301  mdegmullem  26305  deg1mul3le  26344  ig1pdvds  26407  aannenlem2  26562  taylfval  26592  radcnvcl  26650  radcnvlt1  26651  radcnvle  26653  xrlimcnp  27203  nmoxr  31233  nmooge0  31234  nmoolb  31238  nmoubi  31239  nmlno0lem  31260  nmopxr  32333  nmfnxr  32346  nmoplb  32374  nmopub  32375  nmfnlb  32391  nmfnleub  32392  nmlnop0iALT  32462  nmopun  32481  branmfn  32572  pjnmopi  32615  xlt2addrd  33217  xreceu  33354  rexdiv  33358  xrsmulgzz  33436  esumcst  34560  icorempo  38092  mblfinlem2  38394  itg2addnc  38410  prdsbnd  38530  rrnequiv  38572  hbtlem2  43952  binomcxplemdvbinom  45164  binomcxplemcvg  45165  binomcxplemnotnn0  45167  suplesup  46156  frexr  46201  zssxr  46213  ssrexr  46247  uzxrd  46277  supminfxr  46279  rpssxr  46295  elicores  46350  ressiocsup  46371  ressioosup  46372  ressiooinf  46374  uzinico  46376  limsupre  46456  limsupresico  46515  limsupmnflem  46535  supcnvlimsup  46555  liminfresico  46586  volicoff  46810  volicofmpt  46812  fourierdlem52  46973  fourierdlem103  47024  fourierdlem104  47025  etransclem48  47097  ioorrnopnlem  47119  fsumlesge0  47192  sge0cl  47196  sge0supre  47204  sge0less  47207  sge0split  47224  sge0seq  47261  volicorescl  47368  ovolval2lem  47458  ovolval5lem2  47468  ovnovollem1  47471  ovnovollem2  47472  iinhoiicclem  47488  iunhoiioolem  47490  iccvonmbllem  47493  vonioolem2  47496  vonioo  47497  vonicclem2  47499  vonicc  47500  pimdecfgtioc  47530  pimincfltioc  47531  pimdecfgtioo  47532  pimincfltioo  47533  smflimsuplem4  47638