Theorem ressxr 9633

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

Syntax hints:   u. cun 3474   C_ wss 3476   {cpr 4029   RRcr 9487   +oocpnf 9621   -oocmnf 9622   RR*cxr 9623

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3115  df-un 3481  df-in 3483  df-ss 3490  df-xr 9628

This theorem is referenced by:  rexpssxrxp  9634  rexr  9635  0xr  9636  rexrd  9639  ltrelxr  9644  supxrre  11515  supxrbnd  11516  supxrgtmnf  11517  supxrre1  11518  supxrre2  11519  infmxrre  11523  iooval2  11558  fzval2  11671  uzsup  11954  hashxrcl  12393  seqcoll  12474  limsupval2  13262  limsupgre  13263  limsupbnd2  13265  rlimuni  13332  rlimcld2  13360  rlimno1  13435  isercolllem2  13447  isercoll  13449  caucvgrlem  13454  summolem2a  13496  ramtlecl  14373  ramxrcl  14390  ismet2  20571  prdsmet  20608  qtopbas  21001  tgqioo  21040  re2ndc  21041  xrsmopn  21052  metdcn2  21079  metdscn2  21096  bndth  21193  ovolunlem1a  21642  ovolunlem1  21643  ovoliunlem1  21648  ovoliun  21651  ovolicc2lem4  21666  voliunlem2  21696  voliunlem3  21697  opnmblALT  21747  vitalilem4  21755  mbfimaopnlem  21797  itg2le  21881  itg2seq  21884  dvfsumrlim  22167  itgsubst  22185  mdegleb  22199  mdeglt  22200  mdegldg  22201  mdegxrcl  22202  mdegcl  22204  mdegaddle  22209  mdegmullem  22213  deg1mul3le  22252  ig1pdvds  22312  aannenlem2  22459  taylfval  22488  radcnvcl  22546  radcnvlt1  22547  radcnvle  22549  xrlimcnp  23026  nmoxr  25357  nmooge0  25358  nmoolb  25362  nmoubi  25363  nmlno0lem  25384  nmopxr  26461  nmfnxr  26474  nmoplb  26502  nmopub  26503  nmfnlb  26519  nmfnleub  26520  nmlnop0iALT  26590  nmopun  26609  branmfn  26700  pjnmopi  26743  xlt2addrd  27246  xreceu  27286  rexdiv  27290  xrsmulgzz  27328  esumcst  27711  signsply0  28148  prodmolem2a  28643  mblfinlem2  29629  itg2addnc  29646  prdsbnd  29892  rrnequiv  29934  hbtlem2  30677  limsupre  31183  fourierdlem52  31459  fourierdlem103  31510  fourierdlem104  31511