Theorem ressxr 11223

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

Syntax hints:   ∪ cun 3902   ⊆ wss 3904  {cpr 4583  ℝcr 11069  +∞cpnf 11210  -∞cmnf 11211  ℝ^*cxr 11212

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-un 3909  df-ss 3921  df-xr 11217

This theorem is referenced by:  rexpssxrxp  11224  rexr  11225  0xr  11226  rexrd  11229  ltrelxr  11240  supxrre  13327  supxrbnd  13328  supxrgtmnf  13329  supxrre1  13330  supxrre2  13331  infxrre  13337  iooval2  13379  fzval2  13512  uzsup  13870  hashxrcl  14367  seqcoll  14474  limsupval2  15490  limsupgre  15491  limsupbnd2  15493  rlimuni  15560  rlimcld2  15588  rlimno1  15664  isercolllem2  15676  isercoll  15678  caucvgrlem  15683  summolem2a  15725  prodmolem2a  15947  ramtlecl  17019  ramxrcl  17036  ismet2  24373  prdsmet  24410  qtopbas  24799  tgqioo  24840  re2ndc  24841  xrsmopn  24853  metdcn2  24880  metdscn2  24898  bndth  25000  ovolunlem1a  25538  ovolunlem1  25539  ovoliunlem1  25544  ovoliun  25547  ovolicc2lem4  25562  voliunlem2  25593  voliunlem3  25594  opnmblALT  25645  vitalilem4  25653  mbfimaopnlem  25697  itg2le  25781  itg2seq  25784  dvfsumrlim  26073  itgsubst  26091  mdegleb  26104  mdeglt  26105  mdegldg  26106  mdegxrcl  26107  mdegcl  26109  mdegaddle  26114  mdegmullem  26118  deg1mul3le  26157  ig1pdvds  26220  aannenlem2  26370  taylfval  26399  radcnvcl  26457  radcnvlt1  26458  radcnvle  26460  xrlimcnp  27010  nmoxr  30915  nmooge0  30916  nmoolb  30920  nmoubi  30921  nmlno0lem  30942  nmopxr  32015  nmfnxr  32028  nmoplb  32056  nmopub  32057  nmfnlb  32073  nmfnleub  32074  nmlnop0iALT  32144  nmopun  32163  branmfn  32254  pjnmopi  32297  xlt2addrd  32911  xreceu  33060  rexdiv  33064  xrsmulgzz  33148  esumcst  34321  icorempo  37809  mblfinlem2  38121  itg2addnc  38137  prdsbnd  38256  rrnequiv  38298  hbtlem2  43665  binomcxplemdvbinom  44893  binomcxplemcvg  44894  binomcxplemnotnn0  44896  suplesup  45879  frexr  45924  zssxr  45936  ssrexr  45970  uzxrd  46000  supminfxr  46002  rpssxr  46018  elicores  46073  ressiocsup  46094  ressioosup  46095  ressiooinf  46097  uzinico  46099  limsupre  46179  limsupresico  46238  limsupmnflem  46258  supcnvlimsup  46278  liminfresico  46309  volicoff  46533  volicofmpt  46535  fourierdlem52  46696  fourierdlem103  46747  fourierdlem104  46748  etransclem48  46820  ioorrnopnlem  46842  fsumlesge0  46915  sge0cl  46919  sge0supre  46927  sge0less  46930  sge0split  46947  sge0seq  46984  volicorescl  47091  ovolval2lem  47181  ovolval5lem2  47191  ovnovollem1  47194  ovnovollem2  47195  iinhoiicclem  47211  iunhoiioolem  47213  iccvonmbllem  47216  vonioolem2  47219  vonioo  47220  vonicclem2  47222  vonicc  47223  pimdecfgtioc  47253  pimincfltioc  47254  pimdecfgtioo  47255  pimincfltioo  47256  smflimsuplem4  47361