Theorem ressxr 11334

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

Syntax hints:   ∪ cun 3974   ⊆ wss 3976  {cpr 4650  ℝcr 11183  +∞cpnf 11321  -∞cmnf 11322  ℝ^*cxr 11323

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-un 3981  df-ss 3993  df-xr 11328

This theorem is referenced by:  rexpssxrxp  11335  rexr  11336  0xr  11337  rexrd  11340  ltrelxr  11351  supxrre  13389  supxrbnd  13390  supxrgtmnf  13391  supxrre1  13392  supxrre2  13393  infxrre  13398  iooval2  13440  fzval2  13570  uzsup  13914  hashxrcl  14406  seqcoll  14513  limsupval2  15526  limsupgre  15527  limsupbnd2  15529  rlimuni  15596  rlimcld2  15624  rlimno1  15702  isercolllem2  15714  isercoll  15716  caucvgrlem  15721  summolem2a  15763  prodmolem2a  15982  ramtlecl  17047  ramxrcl  17064  ismet2  24364  prdsmet  24401  qtopbas  24801  tgqioo  24841  re2ndc  24842  xrsmopn  24853  metdcn2  24880  metdscn2  24898  bndth  25009  ovolunlem1a  25550  ovolunlem1  25551  ovoliunlem1  25556  ovoliun  25559  ovolicc2lem4  25574  voliunlem2  25605  voliunlem3  25606  opnmblALT  25657  vitalilem4  25665  mbfimaopnlem  25709  itg2le  25794  itg2seq  25797  dvfsumrlim  26092  itgsubst  26110  mdegleb  26123  mdeglt  26124  mdegldg  26125  mdegxrcl  26126  mdegcl  26128  mdegaddle  26133  mdegmullem  26137  deg1mul3le  26176  ig1pdvds  26239  aannenlem2  26389  taylfval  26418  radcnvcl  26478  radcnvlt1  26479  radcnvle  26481  xrlimcnp  27029  nmoxr  30798  nmooge0  30799  nmoolb  30803  nmoubi  30804  nmlno0lem  30825  nmopxr  31898  nmfnxr  31911  nmoplb  31939  nmopub  31940  nmfnlb  31956  nmfnleub  31957  nmlnop0iALT  32027  nmopun  32046  branmfn  32137  pjnmopi  32180  xlt2addrd  32765  xreceu  32886  rexdiv  32890  xrsmulgzz  32992  esumcst  34027  icorempo  37317  mblfinlem2  37618  itg2addnc  37634  prdsbnd  37753  rrnequiv  37795  hbtlem2  43081  binomcxplemdvbinom  44322  binomcxplemcvg  44323  binomcxplemnotnn0  44325  suplesup  45254  frexr  45300  zssxr  45312  ssrexr  45347  uzxrd  45377  supminfxr  45379  rpssxr  45396  elicores  45451  ressiocsup  45472  ressioosup  45473  ressiooinf  45475  uzinico  45478  limsupre  45562  limsupresico  45621  limsupmnflem  45641  limsupvaluz2  45659  supcnvlimsup  45661  liminfresico  45692  volicoff  45916  volicofmpt  45918  fourierdlem52  46079  fourierdlem103  46130  fourierdlem104  46131  etransclem48  46203  ioorrnopnlem  46225  fsumlesge0  46298  sge0cl  46302  sge0supre  46310  sge0less  46313  sge0split  46330  sge0seq  46367  hoicvr  46469  volicorescl  46474  ovolval2lem  46564  ovolval5lem2  46574  ovnovollem1  46577  ovnovollem2  46578  iinhoiicclem  46594  iunhoiioolem  46596  iccvonmbllem  46599  vonioolem2  46602  vonioo  46603  vonicclem2  46605  vonicc  46606  pimdecfgtioc  46636  pimincfltioc  46637  pimdecfgtioo  46638  pimincfltioo  46639  smflimsuplem4  46744