Theorem ressxr 9085

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

Syntax hints:   u. cun 3278   C_ wss 3280   {cpr 3775   RRcr 8945   +oocpnf 9073   -oocmnf 9074   RR*cxr 9075

This theorem is referenced by:  rexr  9086  0xr  9087  rexrd  9090  ltrelxr  9095  supxrre  10862  supxrbnd  10863  supxrgtmnf  10864  supxrre1  10865  supxrre2  10866  infmxrre  10870  iooval2  10905  fzval2  11002  uzsup  11199  hashxrcl  11595  seqcoll  11667  limsupval2  12229  limsupgre  12230  limsupbnd2  12232  rlimuni  12299  rlimcld2  12327  rlimno1  12402  isercolllem2  12414  isercoll  12416  caucvgrlem  12421  summolem2a  12464  ramtlecl  13323  ramxrcl  13340  ismet2  18316  prdsmet  18353  qtopbas  18746  tgqioo  18784  re2ndc  18785  xrsdsre  18794  xrsmopn  18796  metdcn2  18823  metdscn2  18840  bndth  18936  ovolfioo  19317  ovolficc  19318  ovolficcss  19319  ovollb  19328  ovolunlem1a  19345  ovolunlem1  19346  ovoliunlem1  19351  ovoliun  19354  ovolicc2lem4  19369  ovolicc2  19371  voliunlem2  19398  voliunlem3  19399  ovolfs2  19416  uniiccdif  19423  uniioovol  19424  uniiccvol  19425  uniioombllem2  19428  uniioombllem3a  19429  uniioombllem3  19430  uniioombllem4  19431  uniioombllem5  19432  uniioombl  19434  dyadmbllem  19444  opnmbllem  19446  opnmblALT  19448  vitalilem4  19456  mbfimaopnlem  19500  itg2le  19584  itg2seq  19587  dvfsumrlim  19868  itgsubst  19886  mdegleb  19940  mdeglt  19941  mdegldg  19942  mdegxrcl  19943  mdegcl  19945  mdegaddle  19950  mdegmullem  19954  deg1mul3le  19992  ig1pdvds  20052  aannenlem2  20199  taylfval  20228  radcnvcl  20286  radcnvlt1  20287  radcnvle  20289  xrlimcnp  20760  nmoxr  22220  nmooge0  22221  nmoolb  22225  nmoubi  22226  nmlno0lem  22247  nmopxr  23322  nmfnxr  23335  nmoplb  23363  nmopub  23364  nmfnlb  23380  nmfnleub  23381  nmlnop0iALT  23451  nmopun  23470  branmfn  23561  pjnmopi  23604  xlt2addrd  24077  xreceu  24121  rexdiv  24125  xrsmulgzz  24153  esumcst  24408  prodmolem2a  25213  mblfinlem  26143  itg2addnc  26158  prdsbnd  26392  rrnequiv  26434  hbtlem2  27196

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-v 2918  df-un 3285  df-in 3287  df-ss 3294  df-xr 9080