Theorem ressxr 11356

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

This proof depends on syntax axioms:   ⊆ wss 3895   ∪ cun 4149  {cpr 4586  ℝcr 11202  +∞cpnf 11343  -∞cmnf 11344  ℝ^*cxr 11345

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3896  df-un 4151  df-xr 11350

This theorem is used by:  rexpssxrxp  11357  rexr  11358  0xr  11359  rexrd  11362  ltrelxr  11373  supxrre  13460  supxrbnd  13461  supxrgtmnf  13462  supxrre1  13463  supxrre2  13464  infxrre  13470  iooval2  13512  fzval2  13645  uzsup  14006  hashxrcl  14504  seqcoll  14612  limsupval2  15652  limsupgre  15653  limsupbnd2  15655  rlimuni  15722  rlimcld2  15750  rlimno1  15826  isercolllem2  15838  isercoll  15840  caucvgrlem  15845  summolem2a  15886  prodmolem2a  16106  ramtlecl  17183  ramxrcl  17200  ismet2  24657  prdsmet  24694  qtopbas  25083  tgqioo  25124  re2ndc  25125  xrsmopn  25137  metdcn2  25164  metdscn2  25182  bndth  25284  ovolunlem1a  25822  ovolunlem1  25823  ovoliunlem1  25828  ovoliun  25831  ovolicc2lem4  25846  voliunlem2  25877  voliunlem3  25878  opnmblALT  25929  vitalilem4  25937  mbfimaopnlem  25981  itg2le  26065  itg2seq  26068  dvfsumrlim  26356  itgsubst  26374  mdegleb  26387  mdeglt  26388  mdegldg  26389  mdegxrcl  26390  mdegcl  26392  mdegaddle  26397  mdegmullem  26401  deg1mul3le  26440  ig1pdvds  26503  aannenlem2  26661  taylfval  26691  radcnvcl  26749  radcnvlt1  26750  radcnvle  26752  xrlimcnp  27301  nmoxr  31373  nmooge0  31374  nmoolb  31378  nmoubi  31379  nmlno0lem  31400  nmopxr  32473  nmfnxr  32486  nmoplb  32514  nmopub  32515  nmfnlb  32531  nmfnleub  32532  nmlnop0iALT  32602  nmopun  32621  branmfn  32712  pjnmopi  32755  xlt2addrd  33397  xreceu  33534  rexdiv  33538  xrsmulgzz  33616  esumcst  34741  icorempo  38367  mblfinlem2  38669  itg2addnc  38685  prdsbnd  38820  rrnequiv  38862  hbtlem2  44219  binomcxplemdvbinom  45430  binomcxplemcvg  45431  binomcxplemnotnn0  45433  suplesup  46444  frexr  46489  zssxr  46501  ssrexr  46535  uzxrd  46565  supminfxr  46567  rpssxr  46583  elicores  46638  ressiocsup  46659  ressioosup  46660  ressiooinf  46662  uzinico  46664  limsupre  46744  limsupresico  46803  limsupmnflem  46823  supcnvlimsup  46843  liminfresico  46874  volicoff  47098  volicofmpt  47100  fourierdlem52  47261  fourierdlem103  47312  fourierdlem104  47313  etransclem48  47385  ioorrnopnlem  47407  fsumlesge0  47480  sge0cl  47484  sge0supre  47492  sge0less  47495  sge0split  47512  sge0seq  47549  volicorescl  47656  ovolval2lem  47746  ovolval5lem2  47756  ovnovollem1  47759  ovnovollem2  47760  iinhoiicclem  47776  iunhoiioolem  47778  iccvonmbllem  47781  vonioolem2  47784  vonioo  47785  vonicclem2  47787  vonicc  47788  pimdecfgtioc  47818  pimincfltioc  47819  pimdecfgtioo  47820  pimincfltioo  47821  smflimsuplem4  47926