Theorem ressxr 10486

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 4039	. 2 ⊢ ℝ ⊆ (ℝ ∪ {+∞, -∞})
2		df-xr 10480	. 2 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
3	1, 2	sseqtr4i 3896	1 ⊢ ℝ ⊆ ℝ*

Syntax hints:   ∪ cun 3829   ⊆ wss 3831  {cpr 4444  ℝcr 10336  +∞cpnf 10473  -∞cmnf 10474  ℝ^*cxr 10475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-ext 2750

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-clab 2759  df-cleq 2771  df-clel 2846  df-nfc 2918  df-v 3417  df-un 3836  df-in 3838  df-ss 3845  df-xr 10480

This theorem is referenced by:  rexpssxrxp  10487  rexr  10488  0xr  10489  rexrd  10492  ltrelxr  10504  supxrre  12539  supxrbnd  12540  supxrgtmnf  12541  supxrre1  12542  supxrre2  12543  infxrre  12548  iooval2  12590  fzval2  12714  uzsup  13049  hashxrcl  13536  seqcoll  13638  limsupval2  14701  limsupgre  14702  limsupbnd2  14704  rlimuni  14771  rlimcld2  14799  rlimno1  14874  isercolllem2  14886  isercoll  14888  caucvgrlem  14893  summolem2a  14935  prodmolem2a  15151  ramtlecl  16195  ramxrcl  16212  ismet2  22649  prdsmet  22686  qtopbas  23074  tgqioo  23114  re2ndc  23115  xrsmopn  23126  metdcn2  23153  metdscn2  23171  bndth  23268  ovolunlem1a  23803  ovolunlem1  23804  ovoliunlem1  23809  ovoliun  23812  ovolicc2lem4  23827  voliunlem2  23858  voliunlem3  23859  opnmblALT  23910  vitalilem4  23918  mbfimaopnlem  23962  itg2le  24046  itg2seq  24049  dvfsumrlim  24334  itgsubst  24352  mdegleb  24364  mdeglt  24365  mdegldg  24366  mdegxrcl  24367  mdegcl  24369  mdegaddle  24374  mdegmullem  24378  deg1mul3le  24416  ig1pdvds  24476  aannenlem2  24624  taylfval  24653  radcnvcl  24711  radcnvlt1  24712  radcnvle  24714  xrlimcnp  25251  nmoxr  28323  nmooge0  28324  nmoolb  28328  nmoubi  28329  nmlno0lem  28350  nmopxr  29427  nmfnxr  29440  nmoplb  29468  nmopub  29469  nmfnlb  29485  nmfnleub  29486  nmlnop0iALT  29556  nmopun  29575  branmfn  29666  pjnmopi  29709  xlt2addrd  30237  xreceu  30347  rexdiv  30351  xrsmulgzz  30397  esumcst  30966  icorempo  34074  mblfinlem2  34371  itg2addnc  34387  prdsbnd  34513  rrnequiv  34555  hbtlem2  39120  binomcxplemdvbinom  40101  binomcxplemcvg  40102  binomcxplemnotnn0  40104  suplesup  41037  frexr  41086  zssxr  41101  ssrexr  41138  uzxrd  41170  supminfxr  41172  rpssxr  41189  elicores  41241  ressiocsup  41262  ressioosup  41263  ressiooinf  41265  uzinico  41268  limsupre  41354  limsupresico  41413  limsuppnfdlem  41414  limsupmnflem  41433  limsupvaluz2  41451  supcnvlimsup  41453  liminfresico  41484  volicoff  41712  volicofmpt  41714  fourierdlem52  41875  fourierdlem103  41926  fourierdlem104  41927  etransclem48  41999  ioorrnopnlem  42021  fsumlesge0  42091  sge0cl  42095  sge0supre  42103  sge0less  42106  sge0split  42123  sge0seq  42160  hoicvr  42262  volicorescl  42267  ovolval2lem  42357  ovolval5lem2  42367  ovnovollem1  42370  ovnovollem2  42371  iinhoiicclem  42387  iunhoiioolem  42389  iccvonmbllem  42392  vonioolem2  42395  vonioo  42396  vonicclem2  42398  vonicc  42399  pimdecfgtioc  42425  pimincfltioc  42426  pimdecfgtioo  42427  pimincfltioo  42428  smflimsuplem4  42529