Theorem ressxr 11218

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

Syntax hints:   ∪ cun 3912   ⊆ wss 3914  {cpr 4591  ℝcr 11067  +∞cpnf 11205  -∞cmnf 11206  ℝ^*cxr 11207

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-un 3919  df-ss 3931  df-xr 11212

This theorem is referenced by:  rexpssxrxp  11219  rexr  11220  0xr  11221  rexrd  11224  ltrelxr  11235  supxrre  13287  supxrbnd  13288  supxrgtmnf  13289  supxrre1  13290  supxrre2  13291  infxrre  13297  iooval2  13339  fzval2  13471  uzsup  13825  hashxrcl  14322  seqcoll  14429  limsupval2  15446  limsupgre  15447  limsupbnd2  15449  rlimuni  15516  rlimcld2  15544  rlimno1  15620  isercolllem2  15632  isercoll  15634  caucvgrlem  15639  summolem2a  15681  prodmolem2a  15900  ramtlecl  16971  ramxrcl  16988  ismet2  24221  prdsmet  24258  qtopbas  24647  tgqioo  24688  re2ndc  24689  xrsmopn  24701  metdcn2  24728  metdscn2  24746  bndth  24857  ovolunlem1a  25397  ovolunlem1  25398  ovoliunlem1  25403  ovoliun  25406  ovolicc2lem4  25421  voliunlem2  25452  voliunlem3  25453  opnmblALT  25504  vitalilem4  25512  mbfimaopnlem  25556  itg2le  25640  itg2seq  25643  dvfsumrlim  25938  itgsubst  25956  mdegleb  25969  mdeglt  25970  mdegldg  25971  mdegxrcl  25972  mdegcl  25974  mdegaddle  25979  mdegmullem  25983  deg1mul3le  26022  ig1pdvds  26085  aannenlem2  26237  taylfval  26266  radcnvcl  26326  radcnvlt1  26327  radcnvle  26329  xrlimcnp  26878  nmoxr  30695  nmooge0  30696  nmoolb  30700  nmoubi  30701  nmlno0lem  30722  nmopxr  31795  nmfnxr  31808  nmoplb  31836  nmopub  31837  nmfnlb  31853  nmfnleub  31854  nmlnop0iALT  31924  nmopun  31943  branmfn  32034  pjnmopi  32077  xlt2addrd  32682  xreceu  32842  rexdiv  32846  xrsmulgzz  32947  esumcst  34053  icorempo  37339  mblfinlem2  37652  itg2addnc  37668  prdsbnd  37787  rrnequiv  37829  hbtlem2  43113  binomcxplemdvbinom  44342  binomcxplemcvg  44343  binomcxplemnotnn0  44345  suplesup  45335  frexr  45381  zssxr  45393  ssrexr  45428  uzxrd  45458  supminfxr  45460  rpssxr  45476  elicores  45531  ressiocsup  45552  ressioosup  45553  ressiooinf  45555  uzinico  45557  limsupre  45639  limsupresico  45698  limsupmnflem  45718  supcnvlimsup  45738  liminfresico  45769  volicoff  45993  volicofmpt  45995  fourierdlem52  46156  fourierdlem103  46207  fourierdlem104  46208  etransclem48  46280  ioorrnopnlem  46302  fsumlesge0  46375  sge0cl  46379  sge0supre  46387  sge0less  46390  sge0split  46407  sge0seq  46444  hoicvr  46546  volicorescl  46551  ovolval2lem  46641  ovolval5lem2  46651  ovnovollem1  46654  ovnovollem2  46655  iinhoiicclem  46671  iunhoiioolem  46673  iccvonmbllem  46676  vonioolem2  46679  vonioo  46680  vonicclem2  46682  vonicc  46683  pimdecfgtioc  46713  pimincfltioc  46714  pimdecfgtioo  46715  pimincfltioo  46716  smflimsuplem4  46821