Theorem ressxr 9414

Description: The standard reals are a subset of the extended reals. (Contributed by NM, 14-Oct-2005.)

Assertion

Ref	Expression
ressxr	|- RR C_ RR*

Proof of Theorem ressxr

Step	Hyp	Ref	Expression
1		ssun1 3507	. 2 |- RR C_ ( RR u. { +oo , -oo } )
2		df-xr 9409	. 2 |- RR* = ( RR u. { +oo , -oo } )
3	1, 2	sseqtr4i 3377	1 |- RR C_ RR*

Syntax hints:   u. cun 3314   C_ wss 3316   {cpr 3867   RRcr 9268   +oocpnf 9402   -oocmnf 9403   RR*cxr 9404

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-v 2964  df-un 3321  df-in 3323  df-ss 3330  df-xr 9409

This theorem is referenced by:  rexpssxrxp  9415  rexr  9416  0xr  9417  rexrd  9420  ltrelxr  9425  supxrre  11277  supxrbnd  11278  supxrgtmnf  11279  supxrre1  11280  supxrre2  11281  infmxrre  11285  iooval2  11320  fzval2  11426  uzsup  11685  hashxrcl  12110  seqcoll  12199  limsupval2  12941  limsupgre  12942  limsupbnd2  12944  rlimuni  13011  rlimcld2  13039  rlimno1  13114  isercolllem2  13126  isercoll  13128  caucvgrlem  13133  summolem2a  13175  ramtlecl  14043  ramxrcl  14060  ismet2  19749  prdsmet  19786  qtopbas  20179  tgqioo  20218  re2ndc  20219  xrsmopn  20230  metdcn2  20257  metdscn2  20274  bndth  20371  ovolunlem1a  20820  ovolunlem1  20821  ovoliunlem1  20826  ovoliun  20829  ovolicc2lem4  20844  voliunlem2  20873  voliunlem3  20874  opnmblALT  20924  vitalilem4  20932  mbfimaopnlem  20974  itg2le  21058  itg2seq  21061  dvfsumrlim  21344  itgsubst  21362  mdegleb  21419  mdeglt  21420  mdegldg  21421  mdegxrcl  21422  mdegcl  21424  mdegaddle  21429  mdegmullem  21433  deg1mul3le  21472  ig1pdvds  21532  aannenlem2  21679  taylfval  21708  radcnvcl  21766  radcnvlt1  21767  radcnvle  21769  xrlimcnp  22246  nmoxr  23988  nmooge0  23989  nmoolb  23993  nmoubi  23994  nmlno0lem  24015  nmopxr  25092  nmfnxr  25105  nmoplb  25133  nmopub  25134  nmfnlb  25150  nmfnleub  25151  nmlnop0iALT  25221  nmopun  25240  branmfn  25331  pjnmopi  25374  xlt2addrd  25875  xreceu  25919  rexdiv  25923  xrsmulgzz  25961  esumcst  26367  signsply0  26799  prodmolem2a  27293  mblfinlem2  28270  itg2addnc  28287  prdsbnd  28533  rrnequiv  28575  hbtlem2  29322