Theorem ressxr 11065

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

Syntax hints:   ∪ cun 3890   ⊆ wss 3892  {cpr 4567  ℝcr 10916  +∞cpnf 11052  -∞cmnf 11053  ℝ^*cxr 11054

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2714  df-cleq 2728  df-clel 2814  df-v 3439  df-un 3897  df-in 3899  df-ss 3909  df-xr 11059

This theorem is referenced by:  rexpssxrxp  11066  rexr  11067  0xr  11068  rexrd  11071  ltrelxr  11082  supxrre  13107  supxrbnd  13108  supxrgtmnf  13109  supxrre1  13110  supxrre2  13111  infxrre  13116  iooval2  13158  fzval2  13288  uzsup  13629  hashxrcl  14117  seqcoll  14223  limsupval2  15234  limsupgre  15235  limsupbnd2  15237  rlimuni  15304  rlimcld2  15332  rlimno1  15410  isercolllem2  15422  isercoll  15424  caucvgrlem  15429  summolem2a  15472  prodmolem2a  15689  ramtlecl  16746  ramxrcl  16763  ismet2  23531  prdsmet  23568  qtopbas  23968  tgqioo  24008  re2ndc  24009  xrsmopn  24020  metdcn2  24047  metdscn2  24065  bndth  24166  ovolunlem1a  24705  ovolunlem1  24706  ovoliunlem1  24711  ovoliun  24714  ovolicc2lem4  24729  voliunlem2  24760  voliunlem3  24761  opnmblALT  24812  vitalilem4  24820  mbfimaopnlem  24864  itg2le  24949  itg2seq  24952  dvfsumrlim  25240  itgsubst  25258  mdegleb  25274  mdeglt  25275  mdegldg  25276  mdegxrcl  25277  mdegcl  25279  mdegaddle  25284  mdegmullem  25288  deg1mul3le  25326  ig1pdvds  25386  aannenlem2  25534  taylfval  25563  radcnvcl  25621  radcnvlt1  25622  radcnvle  25624  xrlimcnp  26163  nmoxr  29173  nmooge0  29174  nmoolb  29178  nmoubi  29179  nmlno0lem  29200  nmopxr  30273  nmfnxr  30286  nmoplb  30314  nmopub  30315  nmfnlb  30331  nmfnleub  30332  nmlnop0iALT  30402  nmopun  30421  branmfn  30512  pjnmopi  30555  xlt2addrd  31126  xreceu  31241  rexdiv  31245  xrsmulgzz  31332  esumcst  32076  icorempo  35566  mblfinlem2  35859  itg2addnc  35875  prdsbnd  35995  rrnequiv  36037  hbtlem2  40987  binomcxplemdvbinom  42009  binomcxplemcvg  42010  binomcxplemnotnn0  42012  suplesup  42926  frexr  42972  zssxr  42985  ssrexr  43020  uzxrd  43050  supminfxr  43052  rpssxr  43069  elicores  43120  ressiocsup  43141  ressioosup  43142  ressiooinf  43144  uzinico  43147  limsupre  43231  limsupresico  43290  limsupmnflem  43310  limsupvaluz2  43328  supcnvlimsup  43330  liminfresico  43361  volicoff  43585  volicofmpt  43587  fourierdlem52  43748  fourierdlem103  43799  fourierdlem104  43800  etransclem48  43872  ioorrnopnlem  43894  fsumlesge0  43965  sge0cl  43969  sge0supre  43977  sge0less  43980  sge0split  43997  sge0seq  44034  hoicvr  44136  volicorescl  44141  ovolval2lem  44231  ovolval5lem2  44241  ovnovollem1  44244  ovnovollem2  44245  iinhoiicclem  44261  iunhoiioolem  44263  iccvonmbllem  44266  vonioolem2  44269  vonioo  44270  vonicclem2  44272  vonicc  44273  pimdecfgtioc  44303  pimincfltioc  44304  pimdecfgtioo  44305  pimincfltioo  44306  smflimsuplem4  44410