Theorem ressxr 9419

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

Syntax hints:   u. cun 3321   C_ wss 3323   {cpr 3874   RRcr 9273   +oocpnf 9407   -oocmnf 9408   RR*cxr 9409

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-v 2969  df-un 3328  df-in 3330  df-ss 3337  df-xr 9414

This theorem is referenced by:  rexpssxrxp  9420  rexr  9421  0xr  9422  rexrd  9425  ltrelxr  9430  supxrre  11282  supxrbnd  11283  supxrgtmnf  11284  supxrre1  11285  supxrre2  11286  infmxrre  11290  iooval2  11325  fzval2  11432  uzsup  11694  hashxrcl  12119  seqcoll  12208  limsupval2  12950  limsupgre  12951  limsupbnd2  12953  rlimuni  13020  rlimcld2  13048  rlimno1  13123  isercolllem2  13135  isercoll  13137  caucvgrlem  13142  summolem2a  13184  ramtlecl  14053  ramxrcl  14070  ismet2  19883  prdsmet  19920  qtopbas  20313  tgqioo  20352  re2ndc  20353  xrsmopn  20364  metdcn2  20391  metdscn2  20408  bndth  20505  ovolunlem1a  20954  ovolunlem1  20955  ovoliunlem1  20960  ovoliun  20963  ovolicc2lem4  20978  voliunlem2  21007  voliunlem3  21008  opnmblALT  21058  vitalilem4  21066  mbfimaopnlem  21108  itg2le  21192  itg2seq  21195  dvfsumrlim  21478  itgsubst  21496  mdegleb  21510  mdeglt  21511  mdegldg  21512  mdegxrcl  21513  mdegcl  21515  mdegaddle  21520  mdegmullem  21524  deg1mul3le  21563  ig1pdvds  21623  aannenlem2  21770  taylfval  21799  radcnvcl  21857  radcnvlt1  21858  radcnvle  21860  xrlimcnp  22337  nmoxr  24117  nmooge0  24118  nmoolb  24122  nmoubi  24123  nmlno0lem  24144  nmopxr  25221  nmfnxr  25234  nmoplb  25262  nmopub  25263  nmfnlb  25279  nmfnleub  25280  nmlnop0iALT  25350  nmopun  25369  branmfn  25460  pjnmopi  25503  xlt2addrd  26002  xreceu  26048  rexdiv  26052  xrsmulgzz  26090  esumcst  26466  signsply0  26904  prodmolem2a  27398  mblfinlem2  28382  itg2addnc  28399  prdsbnd  28645  rrnequiv  28687  hbtlem2  29433