Theorem ressxr 11264

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

Syntax hints:   ∪ cun 3947   ⊆ wss 3949  {cpr 4631  ℝcr 11113  +∞cpnf 11251  -∞cmnf 11252  ℝ^*cxr 11253

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 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-v 3474  df-un 3954  df-in 3956  df-ss 3966  df-xr 11258

This theorem is referenced by:  rexpssxrxp  11265  rexr  11266  0xr  11267  rexrd  11270  ltrelxr  11281  supxrre  13312  supxrbnd  13313  supxrgtmnf  13314  supxrre1  13315  supxrre2  13316  infxrre  13321  iooval2  13363  fzval2  13493  uzsup  13834  hashxrcl  14323  seqcoll  14431  limsupval2  15430  limsupgre  15431  limsupbnd2  15433  rlimuni  15500  rlimcld2  15528  rlimno1  15606  isercolllem2  15618  isercoll  15620  caucvgrlem  15625  summolem2a  15667  prodmolem2a  15884  ramtlecl  16939  ramxrcl  16956  ismet2  24061  prdsmet  24098  qtopbas  24498  tgqioo  24538  re2ndc  24539  xrsmopn  24550  metdcn2  24577  metdscn2  24595  bndth  24706  ovolunlem1a  25247  ovolunlem1  25248  ovoliunlem1  25253  ovoliun  25256  ovolicc2lem4  25271  voliunlem2  25302  voliunlem3  25303  opnmblALT  25354  vitalilem4  25362  mbfimaopnlem  25406  itg2le  25491  itg2seq  25494  dvfsumrlim  25782  itgsubst  25800  mdegleb  25816  mdeglt  25817  mdegldg  25818  mdegxrcl  25819  mdegcl  25821  mdegaddle  25826  mdegmullem  25830  deg1mul3le  25868  ig1pdvds  25928  aannenlem2  26076  taylfval  26105  radcnvcl  26163  radcnvlt1  26164  radcnvle  26166  xrlimcnp  26707  nmoxr  30284  nmooge0  30285  nmoolb  30289  nmoubi  30290  nmlno0lem  30311  nmopxr  31384  nmfnxr  31397  nmoplb  31425  nmopub  31426  nmfnlb  31442  nmfnleub  31443  nmlnop0iALT  31513  nmopun  31532  branmfn  31623  pjnmopi  31666  xlt2addrd  32236  xreceu  32353  rexdiv  32357  xrsmulgzz  32444  esumcst  33357  icorempo  36537  mblfinlem2  36831  itg2addnc  36847  prdsbnd  36966  rrnequiv  37008  hbtlem2  42170  binomcxplemdvbinom  43416  binomcxplemcvg  43417  binomcxplemnotnn0  43419  suplesup  44349  frexr  44395  zssxr  44407  ssrexr  44442  uzxrd  44472  supminfxr  44474  rpssxr  44491  elicores  44546  ressiocsup  44567  ressioosup  44568  ressiooinf  44570  uzinico  44573  limsupre  44657  limsupresico  44716  limsupmnflem  44736  limsupvaluz2  44754  supcnvlimsup  44756  liminfresico  44787  volicoff  45011  volicofmpt  45013  fourierdlem52  45174  fourierdlem103  45225  fourierdlem104  45226  etransclem48  45298  ioorrnopnlem  45320  fsumlesge0  45393  sge0cl  45397  sge0supre  45405  sge0less  45408  sge0split  45425  sge0seq  45462  hoicvr  45564  volicorescl  45569  ovolval2lem  45659  ovolval5lem2  45669  ovnovollem1  45672  ovnovollem2  45673  iinhoiicclem  45689  iunhoiioolem  45691  iccvonmbllem  45694  vonioolem2  45697  vonioo  45698  vonicclem2  45700  vonicc  45701  pimdecfgtioc  45731  pimincfltioc  45732  pimdecfgtioo  45733  pimincfltioo  45734  smflimsuplem4  45839