Theorem ressxr 11383

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

This proof depends on syntax axioms:   ⊆ wss 3900   ∪ cun 4152  {cpr 4590  ℝcr 11229  +∞cpnf 11370  -∞cmnf 11371  ℝ^*cxr 11372

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-ss 3901  df-un 4154  df-xr 11377

This theorem is used by:  rexpssxrxp  11384  rexr  11385  0xr  11386  rexrd  11389  ltrelxr  11400  supxrre  13487  supxrbnd  13488  supxrgtmnf  13489  supxrre1  13490  supxrre2  13491  infxrre  13497  iooval2  13539  fzval2  13672  uzsup  14033  hashxrcl  14531  seqcoll  14639  limsupval2  15679  limsupgre  15680  limsupbnd2  15682  rlimuni  15749  rlimcld2  15777  rlimno1  15853  isercolllem2  15865  isercoll  15867  caucvgrlem  15872  summolem2a  15913  prodmolem2a  16133  ramtlecl  17210  ramxrcl  17227  ismet2  24685  prdsmet  24722  qtopbas  25111  tgqioo  25152  re2ndc  25153  xrsmopn  25165  metdcn2  25192  metdscn2  25210  bndth  25312  ovolunlem1a  25850  ovolunlem1  25851  ovoliunlem1  25856  ovoliun  25859  ovolicc2lem4  25874  voliunlem2  25905  voliunlem3  25906  opnmblALT  25957  vitalilem4  25965  mbfimaopnlem  26009  itg2le  26093  itg2seq  26096  dvfsumrlim  26384  itgsubst  26402  mdegleb  26415  mdeglt  26416  mdegldg  26417  mdegxrcl  26418  mdegcl  26420  mdegaddle  26425  mdegmullem  26429  deg1mul3le  26468  ig1pdvds  26531  aannenlem2  26689  taylfval  26719  radcnvcl  26777  radcnvlt1  26778  radcnvle  26780  xrlimcnp  27329  nmoxr  31401  nmooge0  31402  nmoolb  31406  nmoubi  31407  nmlno0lem  31428  nmopxr  32501  nmfnxr  32514  nmoplb  32542  nmopub  32543  nmfnlb  32559  nmfnleub  32560  nmlnop0iALT  32630  nmopun  32649  branmfn  32740  pjnmopi  32783  xlt2addrd  33424  xreceu  33561  rexdiv  33565  xrsmulgzz  33646  esumcst  34778  icorempo  38479  mblfinlem2  38781  itg2addnc  38797  prdsbnd  38930  rrnequiv  38972  hbtlem2  44329  binomcxplemdvbinom  45540  binomcxplemcvg  45541  binomcxplemnotnn0  45543  suplesup  46566  frexr  46611  zssxr  46623  ssrexr  46657  uzxrd  46687  supminfxr  46689  rpssxr  46705  elicores  46760  ressiocsup  46781  ressioosup  46782  ressiooinf  46784  uzinico  46786  limsupre  46866  limsupresico  46925  limsupmnflem  46945  supcnvlimsup  46965  liminfresico  46996  volicoff  47220  volicofmpt  47222  fourierdlem52  47383  fourierdlem103  47434  fourierdlem104  47435  etransclem48  47507  ioorrnopnlem  47529  fsumlesge0  47602  sge0cl  47606  sge0supre  47614  sge0less  47617  sge0split  47634  sge0seq  47671  volicorescl  47778  ovolval2lem  47868  ovolval5lem2  47878  ovnovollem1  47881  ovnovollem2  47882  iinhoiicclem  47898  iunhoiioolem  47900  iccvonmbllem  47903  vonioolem2  47906  vonioo  47907  vonicclem2  47909  vonicc  47910  pimdecfgtioc  47940  pimincfltioc  47941  pimdecfgtioo  47942  pimincfltioo  47943  smflimsuplem4  48048