Theorem ressxr 11190

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

Syntax hints:   ∪ cun 3901   ⊆ wss 3903  {cpr 4584  ℝcr 11039  +∞cpnf 11177  -∞cmnf 11178  ℝ^*cxr 11179

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-un 3908  df-ss 3920  df-xr 11184

This theorem is referenced by:  rexpssxrxp  11191  rexr  11192  0xr  11193  rexrd  11196  ltrelxr  11207  supxrre  13256  supxrbnd  13257  supxrgtmnf  13258  supxrre1  13259  supxrre2  13260  infxrre  13266  iooval2  13308  fzval2  13440  uzsup  13797  hashxrcl  14294  seqcoll  14401  limsupval2  15417  limsupgre  15418  limsupbnd2  15420  rlimuni  15487  rlimcld2  15515  rlimno1  15591  isercolllem2  15603  isercoll  15605  caucvgrlem  15610  summolem2a  15652  prodmolem2a  15871  ramtlecl  16942  ramxrcl  16959  ismet2  24294  prdsmet  24331  qtopbas  24720  tgqioo  24761  re2ndc  24762  xrsmopn  24774  metdcn2  24801  metdscn2  24819  bndth  24930  ovolunlem1a  25470  ovolunlem1  25471  ovoliunlem1  25476  ovoliun  25479  ovolicc2lem4  25494  voliunlem2  25525  voliunlem3  25526  opnmblALT  25577  vitalilem4  25585  mbfimaopnlem  25629  itg2le  25713  itg2seq  25716  dvfsumrlim  26011  itgsubst  26029  mdegleb  26042  mdeglt  26043  mdegldg  26044  mdegxrcl  26045  mdegcl  26047  mdegaddle  26052  mdegmullem  26056  deg1mul3le  26095  ig1pdvds  26158  aannenlem2  26310  taylfval  26339  radcnvcl  26399  radcnvlt1  26400  radcnvle  26402  xrlimcnp  26951  nmoxr  30860  nmooge0  30861  nmoolb  30865  nmoubi  30866  nmlno0lem  30887  nmopxr  31960  nmfnxr  31973  nmoplb  32001  nmopub  32002  nmfnlb  32018  nmfnleub  32019  nmlnop0iALT  32089  nmopun  32108  branmfn  32199  pjnmopi  32242  xlt2addrd  32856  xreceu  33020  rexdiv  33024  xrsmulgzz  33108  esumcst  34247  icorempo  37633  mblfinlem2  37938  itg2addnc  37954  prdsbnd  38073  rrnequiv  38115  hbtlem2  43510  binomcxplemdvbinom  44738  binomcxplemcvg  44739  binomcxplemnotnn0  44741  suplesup  45727  frexr  45772  zssxr  45784  ssrexr  45819  uzxrd  45849  supminfxr  45851  rpssxr  45867  elicores  45922  ressiocsup  45943  ressioosup  45944  ressiooinf  45946  uzinico  45948  limsupre  46028  limsupresico  46087  limsupmnflem  46107  supcnvlimsup  46127  liminfresico  46158  volicoff  46382  volicofmpt  46384  fourierdlem52  46545  fourierdlem103  46596  fourierdlem104  46597  etransclem48  46669  ioorrnopnlem  46691  fsumlesge0  46764  sge0cl  46768  sge0supre  46776  sge0less  46779  sge0split  46796  sge0seq  46833  volicorescl  46940  ovolval2lem  47030  ovolval5lem2  47040  ovnovollem1  47043  ovnovollem2  47044  iinhoiicclem  47060  iunhoiioolem  47062  iccvonmbllem  47065  vonioolem2  47068  vonioo  47069  vonicclem2  47071  vonicc  47072  pimdecfgtioc  47102  pimincfltioc  47103  pimdecfgtioo  47104  pimincfltioo  47105  smflimsuplem4  47210