Theorem ressxr 11099

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

Syntax hints:   ∪ cun 3895   ⊆ wss 3897  {cpr 4573  ℝcr 10950  +∞cpnf 11086  -∞cmnf 11087  ℝ^*cxr 11088

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2708

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3443  df-un 3902  df-in 3904  df-ss 3914  df-xr 11093

This theorem is referenced by:  rexpssxrxp  11100  rexr  11101  0xr  11102  rexrd  11105  ltrelxr  11116  supxrre  13141  supxrbnd  13142  supxrgtmnf  13143  supxrre1  13144  supxrre2  13145  infxrre  13150  iooval2  13192  fzval2  13322  uzsup  13663  hashxrcl  14151  seqcoll  14257  limsupval2  15268  limsupgre  15269  limsupbnd2  15271  rlimuni  15338  rlimcld2  15366  rlimno1  15444  isercolllem2  15456  isercoll  15458  caucvgrlem  15463  summolem2a  15506  prodmolem2a  15723  ramtlecl  16778  ramxrcl  16795  ismet2  23569  prdsmet  23606  qtopbas  24006  tgqioo  24046  re2ndc  24047  xrsmopn  24058  metdcn2  24085  metdscn2  24103  bndth  24204  ovolunlem1a  24743  ovolunlem1  24744  ovoliunlem1  24749  ovoliun  24752  ovolicc2lem4  24767  voliunlem2  24798  voliunlem3  24799  opnmblALT  24850  vitalilem4  24858  mbfimaopnlem  24902  itg2le  24987  itg2seq  24990  dvfsumrlim  25278  itgsubst  25296  mdegleb  25312  mdeglt  25313  mdegldg  25314  mdegxrcl  25315  mdegcl  25317  mdegaddle  25322  mdegmullem  25326  deg1mul3le  25364  ig1pdvds  25424  aannenlem2  25572  taylfval  25601  radcnvcl  25659  radcnvlt1  25660  radcnvle  25662  xrlimcnp  26201  nmoxr  29264  nmooge0  29265  nmoolb  29269  nmoubi  29270  nmlno0lem  29291  nmopxr  30364  nmfnxr  30377  nmoplb  30405  nmopub  30406  nmfnlb  30422  nmfnleub  30423  nmlnop0iALT  30493  nmopun  30512  branmfn  30603  pjnmopi  30646  xlt2addrd  31216  xreceu  31331  rexdiv  31335  xrsmulgzz  31422  esumcst  32171  icorempo  35594  mblfinlem2  35887  itg2addnc  35903  prdsbnd  36023  rrnequiv  36065  hbtlem2  41166  binomcxplemdvbinom  42205  binomcxplemcvg  42206  binomcxplemnotnn0  42208  suplesup  43127  frexr  43173  zssxr  43186  ssrexr  43221  uzxrd  43251  supminfxr  43253  rpssxr  43270  elicores  43321  ressiocsup  43342  ressioosup  43343  ressiooinf  43345  uzinico  43348  limsupre  43432  limsupresico  43491  limsupmnflem  43511  limsupvaluz2  43529  supcnvlimsup  43531  liminfresico  43562  volicoff  43786  volicofmpt  43788  fourierdlem52  43949  fourierdlem103  44000  fourierdlem104  44001  etransclem48  44073  ioorrnopnlem  44095  fsumlesge0  44166  sge0cl  44170  sge0supre  44178  sge0less  44181  sge0split  44198  sge0seq  44235  hoicvr  44337  volicorescl  44342  ovolval2lem  44432  ovolval5lem2  44442  ovnovollem1  44445  ovnovollem2  44446  iinhoiicclem  44462  iunhoiioolem  44464  iccvonmbllem  44467  vonioolem2  44470  vonioo  44471  vonicclem2  44473  vonicc  44474  pimdecfgtioc  44504  pimincfltioc  44505  pimdecfgtioo  44506  pimincfltioo  44507  smflimsuplem4  44612