Theorem ressxr 11305

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

Syntax hints:   ∪ cun 3949   ⊆ wss 3951  {cpr 4628  ℝcr 11154  +∞cpnf 11292  -∞cmnf 11293  ℝ^*cxr 11294

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-un 3956  df-ss 3968  df-xr 11299

This theorem is referenced by:  rexpssxrxp  11306  rexr  11307  0xr  11308  rexrd  11311  ltrelxr  11322  supxrre  13369  supxrbnd  13370  supxrgtmnf  13371  supxrre1  13372  supxrre2  13373  infxrre  13378  iooval2  13420  fzval2  13550  uzsup  13903  hashxrcl  14396  seqcoll  14503  limsupval2  15516  limsupgre  15517  limsupbnd2  15519  rlimuni  15586  rlimcld2  15614  rlimno1  15690  isercolllem2  15702  isercoll  15704  caucvgrlem  15709  summolem2a  15751  prodmolem2a  15970  ramtlecl  17038  ramxrcl  17055  ismet2  24343  prdsmet  24380  qtopbas  24780  tgqioo  24821  re2ndc  24822  xrsmopn  24834  metdcn2  24861  metdscn2  24879  bndth  24990  ovolunlem1a  25531  ovolunlem1  25532  ovoliunlem1  25537  ovoliun  25540  ovolicc2lem4  25555  voliunlem2  25586  voliunlem3  25587  opnmblALT  25638  vitalilem4  25646  mbfimaopnlem  25690  itg2le  25774  itg2seq  25777  dvfsumrlim  26072  itgsubst  26090  mdegleb  26103  mdeglt  26104  mdegldg  26105  mdegxrcl  26106  mdegcl  26108  mdegaddle  26113  mdegmullem  26117  deg1mul3le  26156  ig1pdvds  26219  aannenlem2  26371  taylfval  26400  radcnvcl  26460  radcnvlt1  26461  radcnvle  26463  xrlimcnp  27011  nmoxr  30785  nmooge0  30786  nmoolb  30790  nmoubi  30791  nmlno0lem  30812  nmopxr  31885  nmfnxr  31898  nmoplb  31926  nmopub  31927  nmfnlb  31943  nmfnleub  31944  nmlnop0iALT  32014  nmopun  32033  branmfn  32124  pjnmopi  32167  xlt2addrd  32762  xreceu  32904  rexdiv  32908  xrsmulgzz  33011  esumcst  34064  icorempo  37352  mblfinlem2  37665  itg2addnc  37681  prdsbnd  37800  rrnequiv  37842  hbtlem2  43136  binomcxplemdvbinom  44372  binomcxplemcvg  44373  binomcxplemnotnn0  44375  suplesup  45350  frexr  45396  zssxr  45408  ssrexr  45443  uzxrd  45473  supminfxr  45475  rpssxr  45491  elicores  45546  ressiocsup  45567  ressioosup  45568  ressiooinf  45570  uzinico  45573  limsupre  45656  limsupresico  45715  limsupmnflem  45735  supcnvlimsup  45755  liminfresico  45786  volicoff  46010  volicofmpt  46012  fourierdlem52  46173  fourierdlem103  46224  fourierdlem104  46225  etransclem48  46297  ioorrnopnlem  46319  fsumlesge0  46392  sge0cl  46396  sge0supre  46404  sge0less  46407  sge0split  46424  sge0seq  46461  hoicvr  46563  volicorescl  46568  ovolval2lem  46658  ovolval5lem2  46668  ovnovollem1  46671  ovnovollem2  46672  iinhoiicclem  46688  iunhoiioolem  46690  iccvonmbllem  46693  vonioolem2  46696  vonioo  46697  vonicclem2  46699  vonicc  46700  pimdecfgtioc  46730  pimincfltioc  46731  pimdecfgtioo  46732  pimincfltioo  46733  smflimsuplem4  46838