Theorem ressxr 9626

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 3653	. 2 |- RR C_ ( RR u. { +oo , -oo } )
2		df-xr 9621	. 2 |- RR* = ( RR u. { +oo , -oo } )
3	1, 2	sseqtr4i 3522	1 |- RR C_ RR*

Syntax hints:   u. cun 3459   C_ wss 3461   {cpr 4018   RRcr 9480   +oocpnf 9614   -oocmnf 9615   RR*cxr 9616

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3108  df-un 3466  df-in 3468  df-ss 3475  df-xr 9621

This theorem is referenced by:  rexpssxrxp  9627  rexr  9628  0xr  9629  rexrd  9632  ltrelxr  9637  supxrre  11522  supxrbnd  11523  supxrgtmnf  11524  supxrre1  11525  supxrre2  11526  infmxrre  11530  iooval2  11565  fzval2  11678  uzsup  11972  hashxrcl  12414  seqcoll  12499  limsupval2  13388  limsupgre  13389  limsupbnd2  13391  rlimuni  13458  rlimcld2  13486  rlimno1  13561  isercolllem2  13573  isercoll  13575  caucvgrlem  13580  summolem2a  13622  prodmolem2a  13826  ramtlecl  14605  ramxrcl  14622  ismet2  21005  prdsmet  21042  qtopbas  21435  tgqioo  21474  re2ndc  21475  xrsmopn  21486  metdcn2  21513  metdscn2  21530  bndth  21627  ovolunlem1a  22076  ovolunlem1  22077  ovoliunlem1  22082  ovoliun  22085  ovolicc2lem4  22100  voliunlem2  22130  voliunlem3  22131  opnmblALT  22181  vitalilem4  22189  mbfimaopnlem  22231  itg2le  22315  itg2seq  22318  dvfsumrlim  22601  itgsubst  22619  mdegleb  22633  mdeglt  22634  mdegldg  22635  mdegxrcl  22636  mdegcl  22638  mdegaddle  22643  mdegmullem  22647  deg1mul3le  22686  ig1pdvds  22746  aannenlem2  22894  taylfval  22923  radcnvcl  22981  radcnvlt1  22982  radcnvle  22984  xrlimcnp  23499  nmoxr  25882  nmooge0  25883  nmoolb  25887  nmoubi  25888  nmlno0lem  25909  nmopxr  26986  nmfnxr  26999  nmoplb  27027  nmopub  27028  nmfnlb  27044  nmfnleub  27045  nmlnop0iALT  27115  nmopun  27134  branmfn  27225  pjnmopi  27268  xlt2addrd  27812  xreceu  27855  rexdiv  27859  xrsmulgzz  27903  esumcst  28295  mblfinlem2  30295  itg2addnc  30312  prdsbnd  30532  rrnequiv  30574  hbtlem2  31317  binomcxplemdvbinom  31502  binomcxplemcvg  31503  binomcxplemnotnn0  31505  limsupre  31889  fourierdlem52  32183  fourierdlem103  32234  fourierdlem104  32235  etransclem48  32307