Theorem ressxr 11277

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

Syntax hints:   ∪ cun 3924   ⊆ wss 3926  {cpr 4603  ℝcr 11126  +∞cpnf 11264  -∞cmnf 11265  ℝ^*cxr 11266

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 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-un 3931  df-ss 3943  df-xr 11271

This theorem is referenced by:  rexpssxrxp  11278  rexr  11279  0xr  11280  rexrd  11283  ltrelxr  11294  supxrre  13341  supxrbnd  13342  supxrgtmnf  13343  supxrre1  13344  supxrre2  13345  infxrre  13351  iooval2  13393  fzval2  13525  uzsup  13878  hashxrcl  14373  seqcoll  14480  limsupval2  15494  limsupgre  15495  limsupbnd2  15497  rlimuni  15564  rlimcld2  15592  rlimno1  15668  isercolllem2  15680  isercoll  15682  caucvgrlem  15687  summolem2a  15729  prodmolem2a  15948  ramtlecl  17018  ramxrcl  17035  ismet2  24270  prdsmet  24307  qtopbas  24696  tgqioo  24737  re2ndc  24738  xrsmopn  24750  metdcn2  24777  metdscn2  24795  bndth  24906  ovolunlem1a  25447  ovolunlem1  25448  ovoliunlem1  25453  ovoliun  25456  ovolicc2lem4  25471  voliunlem2  25502  voliunlem3  25503  opnmblALT  25554  vitalilem4  25562  mbfimaopnlem  25606  itg2le  25690  itg2seq  25693  dvfsumrlim  25988  itgsubst  26006  mdegleb  26019  mdeglt  26020  mdegldg  26021  mdegxrcl  26022  mdegcl  26024  mdegaddle  26029  mdegmullem  26033  deg1mul3le  26072  ig1pdvds  26135  aannenlem2  26287  taylfval  26316  radcnvcl  26376  radcnvlt1  26377  radcnvle  26379  xrlimcnp  26928  nmoxr  30693  nmooge0  30694  nmoolb  30698  nmoubi  30699  nmlno0lem  30720  nmopxr  31793  nmfnxr  31806  nmoplb  31834  nmopub  31835  nmfnlb  31851  nmfnleub  31852  nmlnop0iALT  31922  nmopun  31941  branmfn  32032  pjnmopi  32075  xlt2addrd  32682  xreceu  32842  rexdiv  32846  xrsmulgzz  32947  esumcst  34040  icorempo  37315  mblfinlem2  37628  itg2addnc  37644  prdsbnd  37763  rrnequiv  37805  hbtlem2  43095  binomcxplemdvbinom  44325  binomcxplemcvg  44326  binomcxplemnotnn0  44328  suplesup  45314  frexr  45360  zssxr  45372  ssrexr  45407  uzxrd  45437  supminfxr  45439  rpssxr  45455  elicores  45510  ressiocsup  45531  ressioosup  45532  ressiooinf  45534  uzinico  45536  limsupre  45618  limsupresico  45677  limsupmnflem  45697  supcnvlimsup  45717  liminfresico  45748  volicoff  45972  volicofmpt  45974  fourierdlem52  46135  fourierdlem103  46186  fourierdlem104  46187  etransclem48  46259  ioorrnopnlem  46281  fsumlesge0  46354  sge0cl  46358  sge0supre  46366  sge0less  46369  sge0split  46386  sge0seq  46423  hoicvr  46525  volicorescl  46530  ovolval2lem  46620  ovolval5lem2  46630  ovnovollem1  46633  ovnovollem2  46634  iinhoiicclem  46650  iunhoiioolem  46652  iccvonmbllem  46655  vonioolem2  46658  vonioo  46659  vonicclem2  46661  vonicc  46662  pimdecfgtioc  46692  pimincfltioc  46693  pimdecfgtioo  46694  pimincfltioo  46695  smflimsuplem4  46800