Theorem ressxr 11271

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

This proof depends on syntax axioms:   ∪ cun 3906   ⊆ wss 3908  {cpr 4596  ℝcr 11117  +∞cpnf 11258  -∞cmnf 11259  ℝ^*cxr 11260

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 2148  ax-9 2156  ax-ext 2738

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 2745  df-cleq 2758  df-clel 2841  df-v 3460  df-un 3913  df-ss 3925  df-xr 11265

This theorem is used by:  rexpssxrxp  11272  rexr  11273  0xr  11274  rexrd  11277  ltrelxr  11288  supxrre  13371  supxrbnd  13372  supxrgtmnf  13373  supxrre1  13374  supxrre2  13375  infxrre  13381  iooval2  13423  fzval2  13556  uzsup  13916  hashxrcl  14413  seqcoll  14521  limsupval2  15557  limsupgre  15558  limsupbnd2  15560  rlimuni  15627  rlimcld2  15655  rlimno1  15731  isercolllem2  15743  isercoll  15745  caucvgrlem  15750  summolem2a  15792  prodmolem2a  16014  ramtlecl  17085  ramxrcl  17102  ismet2  24527  prdsmet  24564  qtopbas  24953  tgqioo  24994  re2ndc  24995  xrsmopn  25007  metdcn2  25034  metdscn2  25052  bndth  25154  ovolunlem1a  25692  ovolunlem1  25693  ovoliunlem1  25698  ovoliun  25701  ovolicc2lem4  25716  voliunlem2  25747  voliunlem3  25748  opnmblALT  25799  vitalilem4  25807  mbfimaopnlem  25851  itg2le  25935  itg2seq  25938  dvfsumrlim  26227  itgsubst  26245  mdegleb  26258  mdeglt  26259  mdegldg  26260  mdegxrcl  26261  mdegcl  26263  mdegaddle  26268  mdegmullem  26272  deg1mul3le  26311  ig1pdvds  26374  aannenlem2  26529  taylfval  26559  radcnvcl  26617  radcnvlt1  26618  radcnvle  26620  xrlimcnp  27170  nmoxr  31155  nmooge0  31156  nmoolb  31160  nmoubi  31161  nmlno0lem  31182  nmopxr  32255  nmfnxr  32268  nmoplb  32296  nmopub  32297  nmfnlb  32313  nmfnleub  32314  nmlnop0iALT  32384  nmopun  32403  branmfn  32494  pjnmopi  32537  xlt2addrd  33141  xreceu  33278  rexdiv  33282  xrsmulgzz  33360  esumcst  34484  icorempo  38038  mblfinlem2  38350  itg2addnc  38366  prdsbnd  38485  rrnequiv  38527  hbtlem2  43892  binomcxplemdvbinom  45104  binomcxplemcvg  45105  binomcxplemnotnn0  45107  suplesup  46096  frexr  46141  zssxr  46153  ssrexr  46187  uzxrd  46217  supminfxr  46219  rpssxr  46235  elicores  46290  ressiocsup  46311  ressioosup  46312  ressiooinf  46314  uzinico  46316  limsupre  46396  limsupresico  46455  limsupmnflem  46475  supcnvlimsup  46495  liminfresico  46526  volicoff  46750  volicofmpt  46752  fourierdlem52  46913  fourierdlem103  46964  fourierdlem104  46965  etransclem48  47037  ioorrnopnlem  47059  fsumlesge0  47132  sge0cl  47136  sge0supre  47144  sge0less  47147  sge0split  47164  sge0seq  47201  volicorescl  47308  ovolval2lem  47398  ovolval5lem2  47408  ovnovollem1  47411  ovnovollem2  47412  iinhoiicclem  47428  iunhoiioolem  47430  iccvonmbllem  47433  vonioolem2  47436  vonioo  47437  vonicclem2  47439  vonicc  47440  pimdecfgtioc  47470  pimincfltioc  47471  pimdecfgtioo  47472  pimincfltioo  47473  smflimsuplem4  47578