Theorem ressxr 11254

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

Syntax hints:   ∪ cun 3904   ⊆ wss 3906  {cpr 4592  ℝcr 11100  +∞cpnf 11241  -∞cmnf 11242  ℝ^*cxr 11243

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-un 3911  df-ss 3923  df-xr 11248

This theorem is referenced by:  rexpssxrxp  11255  rexr  11256  0xr  11257  rexrd  11260  ltrelxr  11271  supxrre  13354  supxrbnd  13355  supxrgtmnf  13356  supxrre1  13357  supxrre2  13358  infxrre  13364  iooval2  13406  fzval2  13539  uzsup  13898  hashxrcl  14395  seqcoll  14503  limsupval2  15533  limsupgre  15534  limsupbnd2  15536  rlimuni  15603  rlimcld2  15631  rlimno1  15707  isercolllem2  15719  isercoll  15721  caucvgrlem  15726  summolem2a  15768  prodmolem2a  15990  ramtlecl  17061  ramxrcl  17078  ismet2  24471  prdsmet  24508  qtopbas  24897  tgqioo  24938  re2ndc  24939  xrsmopn  24951  metdcn2  24978  metdscn2  24996  bndth  25098  ovolunlem1a  25636  ovolunlem1  25637  ovoliunlem1  25642  ovoliun  25645  ovolicc2lem4  25660  voliunlem2  25691  voliunlem3  25692  opnmblALT  25743  vitalilem4  25751  mbfimaopnlem  25795  itg2le  25879  itg2seq  25882  dvfsumrlim  26171  itgsubst  26189  mdegleb  26202  mdeglt  26203  mdegldg  26204  mdegxrcl  26205  mdegcl  26207  mdegaddle  26212  mdegmullem  26216  deg1mul3le  26255  ig1pdvds  26318  aannenlem2  26473  taylfval  26503  radcnvcl  26561  radcnvlt1  26562  radcnvle  26564  xrlimcnp  27114  nmoxr  31099  nmooge0  31100  nmoolb  31104  nmoubi  31105  nmlno0lem  31126  nmopxr  32199  nmfnxr  32212  nmoplb  32240  nmopub  32241  nmfnlb  32257  nmfnleub  32258  nmlnop0iALT  32328  nmopun  32347  branmfn  32438  pjnmopi  32481  xlt2addrd  33085  xreceu  33222  rexdiv  33226  xrsmulgzz  33310  esumcst  34434  icorempo  37978  mblfinlem2  38290  itg2addnc  38306  prdsbnd  38425  rrnequiv  38467  hbtlem2  43834  binomcxplemdvbinom  45046  binomcxplemcvg  45047  binomcxplemnotnn0  45049  suplesup  46038  frexr  46083  zssxr  46095  ssrexr  46129  uzxrd  46159  supminfxr  46161  rpssxr  46177  elicores  46232  ressiocsup  46253  ressioosup  46254  ressiooinf  46256  uzinico  46258  limsupre  46338  limsupresico  46397  limsupmnflem  46417  supcnvlimsup  46437  liminfresico  46468  volicoff  46692  volicofmpt  46694  fourierdlem52  46855  fourierdlem103  46906  fourierdlem104  46907  etransclem48  46979  ioorrnopnlem  47001  fsumlesge0  47074  sge0cl  47078  sge0supre  47086  sge0less  47089  sge0split  47106  sge0seq  47143  volicorescl  47250  ovolval2lem  47340  ovolval5lem2  47350  ovnovollem1  47353  ovnovollem2  47354  iinhoiicclem  47370  iunhoiioolem  47372  iccvonmbllem  47375  vonioolem2  47378  vonioo  47379  vonicclem2  47381  vonicc  47382  pimdecfgtioc  47412  pimincfltioc  47413  pimdecfgtioo  47414  pimincfltioo  47415  smflimsuplem4  47520