Theorem ressxr 10685

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

Syntax hints:   ∪ cun 3934   ⊆ wss 3936  {cpr 4569  ℝcr 10536  +∞cpnf 10672  -∞cmnf 10673  ℝ^*cxr 10674

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-un 3941  df-in 3943  df-ss 3952  df-xr 10679

This theorem is referenced by:  rexpssxrxp  10686  rexr  10687  0xr  10688  rexrd  10691  ltrelxr  10702  supxrre  12721  supxrbnd  12722  supxrgtmnf  12723  supxrre1  12724  supxrre2  12725  infxrre  12730  iooval2  12772  fzval2  12896  uzsup  13232  hashxrcl  13719  seqcoll  13823  limsupval2  14837  limsupgre  14838  limsupbnd2  14840  rlimuni  14907  rlimcld2  14935  rlimno1  15010  isercolllem2  15022  isercoll  15024  caucvgrlem  15029  summolem2a  15072  prodmolem2a  15288  ramtlecl  16336  ramxrcl  16353  ismet2  22943  prdsmet  22980  qtopbas  23368  tgqioo  23408  re2ndc  23409  xrsmopn  23420  metdcn2  23447  metdscn2  23465  bndth  23562  ovolunlem1a  24097  ovolunlem1  24098  ovoliunlem1  24103  ovoliun  24106  ovolicc2lem4  24121  voliunlem2  24152  voliunlem3  24153  opnmblALT  24204  vitalilem4  24212  mbfimaopnlem  24256  itg2le  24340  itg2seq  24343  dvfsumrlim  24628  itgsubst  24646  mdegleb  24658  mdeglt  24659  mdegldg  24660  mdegxrcl  24661  mdegcl  24663  mdegaddle  24668  mdegmullem  24672  deg1mul3le  24710  ig1pdvds  24770  aannenlem2  24918  taylfval  24947  radcnvcl  25005  radcnvlt1  25006  radcnvle  25008  xrlimcnp  25546  nmoxr  28543  nmooge0  28544  nmoolb  28548  nmoubi  28549  nmlno0lem  28570  nmopxr  29643  nmfnxr  29656  nmoplb  29684  nmopub  29685  nmfnlb  29701  nmfnleub  29702  nmlnop0iALT  29772  nmopun  29791  branmfn  29882  pjnmopi  29925  xlt2addrd  30482  xreceu  30598  rexdiv  30602  xrsmulgzz  30665  esumcst  31322  icorempo  34635  mblfinlem2  34945  itg2addnc  34961  prdsbnd  35086  rrnequiv  35128  hbtlem2  39744  binomcxplemdvbinom  40705  binomcxplemcvg  40706  binomcxplemnotnn0  40708  suplesup  41627  frexr  41675  zssxr  41690  ssrexr  41726  uzxrd  41758  supminfxr  41760  rpssxr  41777  elicores  41829  ressiocsup  41850  ressioosup  41851  ressiooinf  41853  uzinico  41856  limsupre  41942  limsupresico  42001  limsupmnflem  42021  limsupvaluz2  42039  supcnvlimsup  42041  liminfresico  42072  volicoff  42300  volicofmpt  42302  fourierdlem52  42463  fourierdlem103  42514  fourierdlem104  42515  etransclem48  42587  ioorrnopnlem  42609  fsumlesge0  42679  sge0cl  42683  sge0supre  42691  sge0less  42694  sge0split  42711  sge0seq  42748  hoicvr  42850  volicorescl  42855  ovolval2lem  42945  ovolval5lem2  42955  ovnovollem1  42958  ovnovollem2  42959  iinhoiicclem  42975  iunhoiioolem  42977  iccvonmbllem  42980  vonioolem2  42983  vonioo  42984  vonicclem2  42986  vonicc  42987  pimdecfgtioc  43013  pimincfltioc  43014  pimdecfgtioo  43015  pimincfltioo  43016  smflimsuplem4  43117