Theorem ressxr 11003

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

Syntax hints:   ∪ cun 3889   ⊆ wss 3891  {cpr 4568  ℝcr 10854  +∞cpnf 10990  -∞cmnf 10991  ℝ^*cxr 10992

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1544  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3432  df-un 3896  df-in 3898  df-ss 3908  df-xr 10997

This theorem is referenced by:  rexpssxrxp  11004  rexr  11005  0xr  11006  rexrd  11009  ltrelxr  11020  supxrre  13043  supxrbnd  13044  supxrgtmnf  13045  supxrre1  13046  supxrre2  13047  infxrre  13052  iooval2  13094  fzval2  13224  uzsup  13564  hashxrcl  14053  seqcoll  14159  limsupval2  15170  limsupgre  15171  limsupbnd2  15173  rlimuni  15240  rlimcld2  15268  rlimno1  15346  isercolllem2  15358  isercoll  15360  caucvgrlem  15365  summolem2a  15408  prodmolem2a  15625  ramtlecl  16682  ramxrcl  16699  ismet2  23467  prdsmet  23504  qtopbas  23904  tgqioo  23944  re2ndc  23945  xrsmopn  23956  metdcn2  23983  metdscn2  24001  bndth  24102  ovolunlem1a  24641  ovolunlem1  24642  ovoliunlem1  24647  ovoliun  24650  ovolicc2lem4  24665  voliunlem2  24696  voliunlem3  24697  opnmblALT  24748  vitalilem4  24756  mbfimaopnlem  24800  itg2le  24885  itg2seq  24888  dvfsumrlim  25176  itgsubst  25194  mdegleb  25210  mdeglt  25211  mdegldg  25212  mdegxrcl  25213  mdegcl  25215  mdegaddle  25220  mdegmullem  25224  deg1mul3le  25262  ig1pdvds  25322  aannenlem2  25470  taylfval  25499  radcnvcl  25557  radcnvlt1  25558  radcnvle  25560  xrlimcnp  26099  nmoxr  29107  nmooge0  29108  nmoolb  29112  nmoubi  29113  nmlno0lem  29134  nmopxr  30207  nmfnxr  30220  nmoplb  30248  nmopub  30249  nmfnlb  30265  nmfnleub  30266  nmlnop0iALT  30336  nmopun  30355  branmfn  30446  pjnmopi  30489  xlt2addrd  31060  xreceu  31175  rexdiv  31179  xrsmulgzz  31266  esumcst  32010  icorempo  35501  mblfinlem2  35794  itg2addnc  35810  prdsbnd  35930  rrnequiv  35972  hbtlem2  40929  binomcxplemdvbinom  41924  binomcxplemcvg  41925  binomcxplemnotnn0  41927  suplesup  42832  frexr  42878  zssxr  42891  ssrexr  42926  uzxrd  42956  supminfxr  42958  rpssxr  42975  elicores  43025  ressiocsup  43046  ressioosup  43047  ressiooinf  43049  uzinico  43052  limsupre  43136  limsupresico  43195  limsupmnflem  43215  limsupvaluz2  43233  supcnvlimsup  43235  liminfresico  43266  volicoff  43490  volicofmpt  43492  fourierdlem52  43653  fourierdlem103  43704  fourierdlem104  43705  etransclem48  43777  ioorrnopnlem  43799  fsumlesge0  43869  sge0cl  43873  sge0supre  43881  sge0less  43884  sge0split  43901  sge0seq  43938  hoicvr  44040  volicorescl  44045  ovolval2lem  44135  ovolval5lem2  44145  ovnovollem1  44148  ovnovollem2  44149  iinhoiicclem  44165  iunhoiioolem  44167  iccvonmbllem  44170  vonioolem2  44173  vonioo  44174  vonicclem2  44176  vonicc  44177  pimdecfgtioc  44203  pimincfltioc  44204  pimdecfgtioo  44205  pimincfltioo  44206  smflimsuplem4  44307