Theorem ressxr 9531

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

Syntax hints:   u. cun 3427   C_ wss 3429   {cpr 3980   RRcr 9385   +oocpnf 9519   -oocmnf 9520   RR*cxr 9521

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-v 3073  df-un 3434  df-in 3436  df-ss 3443  df-xr 9526

This theorem is referenced by:  rexpssxrxp  9532  rexr  9533  0xr  9534  rexrd  9537  ltrelxr  9542  supxrre  11394  supxrbnd  11395  supxrgtmnf  11396  supxrre1  11397  supxrre2  11398  infmxrre  11402  iooval2  11437  fzval2  11550  uzsup  11812  hashxrcl  12237  seqcoll  12327  limsupval2  13069  limsupgre  13070  limsupbnd2  13072  rlimuni  13139  rlimcld2  13167  rlimno1  13242  isercolllem2  13254  isercoll  13256  caucvgrlem  13261  summolem2a  13303  ramtlecl  14172  ramxrcl  14189  ismet2  20033  prdsmet  20070  qtopbas  20463  tgqioo  20502  re2ndc  20503  xrsmopn  20514  metdcn2  20541  metdscn2  20558  bndth  20655  ovolunlem1a  21104  ovolunlem1  21105  ovoliunlem1  21110  ovoliun  21113  ovolicc2lem4  21128  voliunlem2  21158  voliunlem3  21159  opnmblALT  21209  vitalilem4  21217  mbfimaopnlem  21259  itg2le  21343  itg2seq  21346  dvfsumrlim  21629  itgsubst  21647  mdegleb  21661  mdeglt  21662  mdegldg  21663  mdegxrcl  21664  mdegcl  21666  mdegaddle  21671  mdegmullem  21675  deg1mul3le  21714  ig1pdvds  21774  aannenlem2  21921  taylfval  21950  radcnvcl  22008  radcnvlt1  22009  radcnvle  22011  xrlimcnp  22488  nmoxr  24311  nmooge0  24312  nmoolb  24316  nmoubi  24317  nmlno0lem  24338  nmopxr  25415  nmfnxr  25428  nmoplb  25456  nmopub  25457  nmfnlb  25473  nmfnleub  25474  nmlnop0iALT  25544  nmopun  25563  branmfn  25654  pjnmopi  25697  xlt2addrd  26195  xreceu  26235  rexdiv  26239  xrsmulgzz  26277  esumcst  26652  signsply0  27089  prodmolem2a  27584  mblfinlem2  28570  itg2addnc  28587  prdsbnd  28833  rrnequiv  28875  hbtlem2  29621