MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ressxr Unicode version

Theorem ressxr 8876
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
StepHypRef Expression
1 ssun1 3338 . 2  |-  RR  C_  ( RR  u.  {  +oo , 
-oo } )
2 df-xr 8871 . 2  |-  RR*  =  ( RR  u.  {  +oo , 
-oo } )
31, 2sseqtr4i 3211 1  |-  RR  C_  RR*
Colors of variables: wff set class
Syntax hints:    u. cun 3150    C_ wss 3152   {cpr 3641   RRcr 8736    +oocpnf 8864    -oocmnf 8865   RR*cxr 8866
This theorem is referenced by:  rexr  8877  0xr  8878  rexrd  8881  ltrelxr  8886  supxrre  10646  supxrbnd  10647  supxrgtmnf  10648  supxrre1  10649  supxrre2  10650  infmxrre  10654  iooval2  10689  fzval2  10785  uzsup  10967  hashxrcl  11351  seqcoll  11401  limsupval2  11954  limsupgre  11955  limsupbnd2  11957  rlimuni  12024  rlimcld2  12052  rlimno1  12127  isercolllem2  12139  isercoll  12141  caucvgrlem  12145  summolem2a  12188  tanhbnd  12441  ramtlecl  13047  ramxrcl  13064  ismet2  17898  prdsmet  17934  qtopbas  18268  tgqioo  18306  re2ndc  18307  xrsdsre  18316  xrsmopn  18318  metdcn2  18344  metdscn2  18361  oprpiece1res2  18450  bndth  18456  pcoass  18522  ovolfioo  18827  ovolficc  18828  ovolficcss  18829  ovollb  18838  ovolunlem1a  18855  ovolunlem1  18856  ovoliunlem1  18861  ovoliun  18864  ovolicc2lem4  18879  ovolicc2  18881  voliunlem2  18908  voliunlem3  18909  ovolfs2  18926  uniiccdif  18933  uniioovol  18934  uniiccvol  18935  uniioombllem2  18938  uniioombllem3a  18939  uniioombllem3  18940  uniioombllem4  18941  uniioombllem5  18942  uniioombl  18944  dyadmbllem  18954  opnmbllem  18956  opnmblALT  18958  vitalilem4  18966  mbfimaopnlem  19010  itg2le  19094  itg2seq  19097  dvfsumrlim  19378  itgsubst  19396  mdegleb  19450  mdeglt  19451  mdegldg  19452  mdegxrcl  19453  mdegcl  19455  mdegaddle  19460  mdegmullem  19464  deg1mul3le  19502  ig1pdvds  19562  aannenlem2  19709  taylfval  19738  radcnvcl  19793  radcnvlt1  19794  radcnvle  19796  sincosq4sgn  19869  tanabsge  19874  sinq12gt0  19875  cosq14gt0  19878  tanord1  19899  tanregt0  19901  ellogrn  19917  argregt0  19964  argimgt0  19966  argimlt0  19967  dvloglem  19995  asinneg  20182  asinsinlem  20187  acoscos  20189  reasinsin  20192  atanlogsublem  20211  atanbndlem  20221  atanbnd  20222  atan1  20224  xrlimcnp  20263  scvxcvx  20280  basellem4  20321  pntibndlem2  20740  padicabvf  20780  padicabvcxp  20781  nmoxr  21344  nmooge0  21345  nmoolb  21349  nmoubi  21350  nmlno0lem  21371  nmopxr  22446  nmfnxr  22459  nmoplb  22487  nmopub  22488  nmfnlb  22504  nmfnleub  22505  nmlnop0iALT  22575  nmopun  22594  branmfn  22685  pjnmopi  22728  xreceu  23105  rexdiv  23109  xlt2addrd  23253  xrsmulgzz  23307  xrge0iifcnv  23315  esumcst  23436  dstrvprob  23672  umgrafi  23874  basexre  25522  altretop  25600  prdsbnd  26517  rrnequiv  26559  hbtlem2  27328
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-un 3157  df-in 3159  df-ss 3166  df-xr 8871
  Copyright terms: Public domain W3C validator