Theorem ressxr 11208

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

Syntax hints:   ∪ cun 3911   ⊆ wss 3913  {cpr 4593  ℝcr 11059  +∞cpnf 11195  -∞cmnf 11196  ℝ^*cxr 11197

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3448  df-un 3918  df-in 3920  df-ss 3930  df-xr 11202

This theorem is referenced by:  rexpssxrxp  11209  rexr  11210  0xr  11211  rexrd  11214  ltrelxr  11225  supxrre  13256  supxrbnd  13257  supxrgtmnf  13258  supxrre1  13259  supxrre2  13260  infxrre  13265  iooval2  13307  fzval2  13437  uzsup  13778  hashxrcl  14267  seqcoll  14375  limsupval2  15374  limsupgre  15375  limsupbnd2  15377  rlimuni  15444  rlimcld2  15472  rlimno1  15550  isercolllem2  15562  isercoll  15564  caucvgrlem  15569  summolem2a  15611  prodmolem2a  15828  ramtlecl  16883  ramxrcl  16900  ismet2  23723  prdsmet  23760  qtopbas  24160  tgqioo  24200  re2ndc  24201  xrsmopn  24212  metdcn2  24239  metdscn2  24257  bndth  24358  ovolunlem1a  24897  ovolunlem1  24898  ovoliunlem1  24903  ovoliun  24906  ovolicc2lem4  24921  voliunlem2  24952  voliunlem3  24953  opnmblALT  25004  vitalilem4  25012  mbfimaopnlem  25056  itg2le  25141  itg2seq  25144  dvfsumrlim  25432  itgsubst  25450  mdegleb  25466  mdeglt  25467  mdegldg  25468  mdegxrcl  25469  mdegcl  25471  mdegaddle  25476  mdegmullem  25480  deg1mul3le  25518  ig1pdvds  25578  aannenlem2  25726  taylfval  25755  radcnvcl  25813  radcnvlt1  25814  radcnvle  25816  xrlimcnp  26355  nmoxr  29771  nmooge0  29772  nmoolb  29776  nmoubi  29777  nmlno0lem  29798  nmopxr  30871  nmfnxr  30884  nmoplb  30912  nmopub  30913  nmfnlb  30929  nmfnleub  30930  nmlnop0iALT  31000  nmopun  31019  branmfn  31110  pjnmopi  31153  xlt2addrd  31731  xreceu  31848  rexdiv  31852  xrsmulgzz  31939  esumcst  32751  icorempo  35895  mblfinlem2  36189  itg2addnc  36205  prdsbnd  36325  rrnequiv  36367  hbtlem2  41509  binomcxplemdvbinom  42755  binomcxplemcvg  42756  binomcxplemnotnn0  42758  suplesup  43694  frexr  43740  zssxr  43752  ssrexr  43787  uzxrd  43817  supminfxr  43819  rpssxr  43836  elicores  43891  ressiocsup  43912  ressioosup  43913  ressiooinf  43915  uzinico  43918  limsupre  44002  limsupresico  44061  limsupmnflem  44081  limsupvaluz2  44099  supcnvlimsup  44101  liminfresico  44132  volicoff  44356  volicofmpt  44358  fourierdlem52  44519  fourierdlem103  44570  fourierdlem104  44571  etransclem48  44643  ioorrnopnlem  44665  fsumlesge0  44738  sge0cl  44742  sge0supre  44750  sge0less  44753  sge0split  44770  sge0seq  44807  hoicvr  44909  volicorescl  44914  ovolval2lem  45004  ovolval5lem2  45014  ovnovollem1  45017  ovnovollem2  45018  iinhoiicclem  45034  iunhoiioolem  45036  iccvonmbllem  45039  vonioolem2  45042  vonioo  45043  vonicclem2  45045  vonicc  45046  pimdecfgtioc  45076  pimincfltioc  45077  pimdecfgtioo  45078  pimincfltioo  45079  smflimsuplem4  45184