Theorem ressxr 11334

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

This proof depends on syntax axioms:   ∪ cun 3897   ⊆ wss 3899  {cpr 4586  ℝcr 11180  +∞cpnf 11321  -∞cmnf 11322  ℝ^*cxr 11323

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 2733

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 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-un 3904  df-ss 3916  df-xr 11328

This theorem is used by:  rexpssxrxp  11335  rexr  11336  0xr  11337  rexrd  11340  ltrelxr  11351  supxrre  13438  supxrbnd  13439  supxrgtmnf  13440  supxrre1  13441  supxrre2  13442  infxrre  13448  iooval2  13490  fzval2  13623  uzsup  13983  hashxrcl  14481  seqcoll  14589  limsupval2  15627  limsupgre  15628  limsupbnd2  15630  rlimuni  15697  rlimcld2  15725  rlimno1  15801  isercolllem2  15813  isercoll  15815  caucvgrlem  15820  summolem2a  15861  prodmolem2a  16081  ramtlecl  17158  ramxrcl  17175  ismet2  24632  prdsmet  24669  qtopbas  25058  tgqioo  25099  re2ndc  25100  xrsmopn  25112  metdcn2  25139  metdscn2  25157  bndth  25259  ovolunlem1a  25797  ovolunlem1  25798  ovoliunlem1  25803  ovoliun  25806  ovolicc2lem4  25821  voliunlem2  25852  voliunlem3  25853  opnmblALT  25904  vitalilem4  25912  mbfimaopnlem  25956  itg2le  26040  itg2seq  26043  dvfsumrlim  26331  itgsubst  26349  mdegleb  26362  mdeglt  26363  mdegldg  26364  mdegxrcl  26365  mdegcl  26367  mdegaddle  26372  mdegmullem  26376  deg1mul3le  26415  ig1pdvds  26478  aannenlem2  26638  taylfval  26668  radcnvcl  26726  radcnvlt1  26727  radcnvle  26729  xrlimcnp  27278  nmoxr  31350  nmooge0  31351  nmoolb  31355  nmoubi  31356  nmlno0lem  31377  nmopxr  32450  nmfnxr  32463  nmoplb  32491  nmopub  32492  nmfnlb  32508  nmfnleub  32509  nmlnop0iALT  32579  nmopun  32598  branmfn  32689  pjnmopi  32732  xlt2addrd  33333  xreceu  33470  rexdiv  33474  xrsmulgzz  33552  esumcst  34677  icorempo  38242  mblfinlem2  38544  itg2addnc  38560  prdsbnd  38695  rrnequiv  38737  hbtlem2  44084  binomcxplemdvbinom  45296  binomcxplemcvg  45297  binomcxplemnotnn0  45299  suplesup  46295  frexr  46340  zssxr  46352  ssrexr  46386  uzxrd  46416  supminfxr  46418  rpssxr  46434  elicores  46489  ressiocsup  46510  ressioosup  46511  ressiooinf  46513  uzinico  46515  limsupre  46595  limsupresico  46654  limsupmnflem  46674  supcnvlimsup  46694  liminfresico  46725  volicoff  46949  volicofmpt  46951  fourierdlem52  47112  fourierdlem103  47163  fourierdlem104  47164  etransclem48  47236  ioorrnopnlem  47258  fsumlesge0  47331  sge0cl  47335  sge0supre  47343  sge0less  47346  sge0split  47363  sge0seq  47400  volicorescl  47507  ovolval2lem  47597  ovolval5lem2  47607  ovnovollem1  47610  ovnovollem2  47611  iinhoiicclem  47627  iunhoiioolem  47629  iccvonmbllem  47632  vonioolem2  47635  vonioo  47636  vonicclem2  47638  vonicc  47639  pimdecfgtioc  47669  pimincfltioc  47670  pimdecfgtioo  47671  pimincfltioo  47672  smflimsuplem4  47777