Theorem ressxr 11176

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

Syntax hints:   ∪ cun 3899   ⊆ wss 3901  {cpr 4582  ℝcr 11025  +∞cpnf 11163  -∞cmnf 11164  ℝ^*cxr 11165

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-un 3906  df-ss 3918  df-xr 11170

This theorem is referenced by:  rexpssxrxp  11177  rexr  11178  0xr  11179  rexrd  11182  ltrelxr  11193  supxrre  13242  supxrbnd  13243  supxrgtmnf  13244  supxrre1  13245  supxrre2  13246  infxrre  13252  iooval2  13294  fzval2  13426  uzsup  13783  hashxrcl  14280  seqcoll  14387  limsupval2  15403  limsupgre  15404  limsupbnd2  15406  rlimuni  15473  rlimcld2  15501  rlimno1  15577  isercolllem2  15589  isercoll  15591  caucvgrlem  15596  summolem2a  15638  prodmolem2a  15857  ramtlecl  16928  ramxrcl  16945  ismet2  24277  prdsmet  24314  qtopbas  24703  tgqioo  24744  re2ndc  24745  xrsmopn  24757  metdcn2  24784  metdscn2  24802  bndth  24913  ovolunlem1a  25453  ovolunlem1  25454  ovoliunlem1  25459  ovoliun  25462  ovolicc2lem4  25477  voliunlem2  25508  voliunlem3  25509  opnmblALT  25560  vitalilem4  25568  mbfimaopnlem  25612  itg2le  25696  itg2seq  25699  dvfsumrlim  25994  itgsubst  26012  mdegleb  26025  mdeglt  26026  mdegldg  26027  mdegxrcl  26028  mdegcl  26030  mdegaddle  26035  mdegmullem  26039  deg1mul3le  26078  ig1pdvds  26141  aannenlem2  26293  taylfval  26322  radcnvcl  26382  radcnvlt1  26383  radcnvle  26385  xrlimcnp  26934  nmoxr  30841  nmooge0  30842  nmoolb  30846  nmoubi  30847  nmlno0lem  30868  nmopxr  31941  nmfnxr  31954  nmoplb  31982  nmopub  31983  nmfnlb  31999  nmfnleub  32000  nmlnop0iALT  32070  nmopun  32089  branmfn  32180  pjnmopi  32223  xlt2addrd  32839  xreceu  33003  rexdiv  33007  xrsmulgzz  33091  esumcst  34220  icorempo  37556  mblfinlem2  37859  itg2addnc  37875  prdsbnd  37994  rrnequiv  38036  hbtlem2  43366  binomcxplemdvbinom  44594  binomcxplemcvg  44595  binomcxplemnotnn0  44597  suplesup  45584  frexr  45629  zssxr  45641  ssrexr  45676  uzxrd  45706  supminfxr  45708  rpssxr  45724  elicores  45779  ressiocsup  45800  ressioosup  45801  ressiooinf  45803  uzinico  45805  limsupre  45885  limsupresico  45944  limsupmnflem  45964  supcnvlimsup  45984  liminfresico  46015  volicoff  46239  volicofmpt  46241  fourierdlem52  46402  fourierdlem103  46453  fourierdlem104  46454  etransclem48  46526  ioorrnopnlem  46548  fsumlesge0  46621  sge0cl  46625  sge0supre  46633  sge0less  46636  sge0split  46653  sge0seq  46690  hoicvr  46792  volicorescl  46797  ovolval2lem  46887  ovolval5lem2  46897  ovnovollem1  46900  ovnovollem2  46901  iinhoiicclem  46917  iunhoiioolem  46919  iccvonmbllem  46922  vonioolem2  46925  vonioo  46926  vonicclem2  46928  vonicc  46929  pimdecfgtioc  46959  pimincfltioc  46960  pimdecfgtioo  46961  pimincfltioo  46962  smflimsuplem4  47067