Theorem ressxr 11241

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

Syntax hints:   ∪ cun 3905   ⊆ wss 3907  {cpr 4587  ℝcr 11087  +∞cpnf 11228  -∞cmnf 11229  ℝ^*cxr 11230

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-un 3912  df-ss 3924  df-xr 11235

This theorem is referenced by:  rexpssxrxp  11242  rexr  11243  0xr  11244  rexrd  11247  ltrelxr  11258  supxrre  13344  supxrbnd  13345  supxrgtmnf  13346  supxrre1  13347  supxrre2  13348  infxrre  13354  iooval2  13396  fzval2  13529  uzsup  13887  hashxrcl  14384  seqcoll  14491  limsupval2  15521  limsupgre  15522  limsupbnd2  15524  rlimuni  15591  rlimcld2  15619  rlimno1  15695  isercolllem2  15707  isercoll  15709  caucvgrlem  15714  summolem2a  15756  prodmolem2a  15978  ramtlecl  17050  ramxrcl  17067  ismet2  24451  prdsmet  24488  qtopbas  24877  tgqioo  24918  re2ndc  24919  xrsmopn  24931  metdcn2  24958  metdscn2  24976  bndth  25078  ovolunlem1a  25616  ovolunlem1  25617  ovoliunlem1  25622  ovoliun  25625  ovolicc2lem4  25640  voliunlem2  25671  voliunlem3  25672  opnmblALT  25723  vitalilem4  25731  mbfimaopnlem  25775  itg2le  25859  itg2seq  25862  dvfsumrlim  26151  itgsubst  26169  mdegleb  26182  mdeglt  26183  mdegldg  26184  mdegxrcl  26185  mdegcl  26187  mdegaddle  26192  mdegmullem  26196  deg1mul3le  26235  ig1pdvds  26298  aannenlem2  26451  taylfval  26480  radcnvcl  26538  radcnvlt1  26539  radcnvle  26541  xrlimcnp  27091  nmoxr  31027  nmooge0  31028  nmoolb  31032  nmoubi  31033  nmlno0lem  31054  nmopxr  32127  nmfnxr  32140  nmoplb  32168  nmopub  32169  nmfnlb  32185  nmfnleub  32186  nmlnop0iALT  32256  nmopun  32275  branmfn  32366  pjnmopi  32409  xlt2addrd  33016  xreceu  33154  rexdiv  33158  xrsmulgzz  33242  esumcst  34370  icorempo  37857  mblfinlem2  38169  itg2addnc  38185  prdsbnd  38304  rrnequiv  38346  hbtlem2  43713  binomcxplemdvbinom  44927  binomcxplemcvg  44928  binomcxplemnotnn0  44930  suplesup  45913  frexr  45958  zssxr  45970  ssrexr  46004  uzxrd  46034  supminfxr  46036  rpssxr  46052  elicores  46107  ressiocsup  46128  ressioosup  46129  ressiooinf  46131  uzinico  46133  limsupre  46213  limsupresico  46272  limsupmnflem  46292  supcnvlimsup  46312  liminfresico  46343  volicoff  46567  volicofmpt  46569  fourierdlem52  46730  fourierdlem103  46781  fourierdlem104  46782  etransclem48  46854  ioorrnopnlem  46876  fsumlesge0  46949  sge0cl  46953  sge0supre  46961  sge0less  46964  sge0split  46981  sge0seq  47018  volicorescl  47125  ovolval2lem  47215  ovolval5lem2  47225  ovnovollem1  47228  ovnovollem2  47229  iinhoiicclem  47245  iunhoiioolem  47247  iccvonmbllem  47250  vonioolem2  47253  vonioo  47254  vonicclem2  47256  vonicc  47257  pimdecfgtioc  47287  pimincfltioc  47288  pimdecfgtioo  47289  pimincfltioo  47290  smflimsuplem4  47395