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

Theorem ressxr 8921
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 3372 . 2  |-  RR  C_  ( RR  u.  {  +oo , 
-oo } )
2 df-xr 8916 . 2  |-  RR*  =  ( RR  u.  {  +oo , 
-oo } )
31, 2sseqtr4i 3245 1  |-  RR  C_  RR*
Colors of variables: wff set class
Syntax hints:    u. cun 3184    C_ wss 3186   {cpr 3675   RRcr 8781    +oocpnf 8909    -oocmnf 8910   RR*cxr 8911
This theorem is referenced by:  rexr  8922  0xr  8923  rexrd  8926  ltrelxr  8931  supxrre  10693  supxrbnd  10694  supxrgtmnf  10695  supxrre1  10696  supxrre2  10697  infmxrre  10701  iooval2  10736  fzval2  10832  uzsup  11014  hashxrcl  11398  seqcoll  11448  limsupval2  12001  limsupgre  12002  limsupbnd2  12004  rlimuni  12071  rlimcld2  12099  rlimno1  12174  isercolllem2  12186  isercoll  12188  caucvgrlem  12192  summolem2a  12235  tanhbnd  12488  ramtlecl  13094  ramxrcl  13111  ismet2  17950  prdsmet  17986  qtopbas  18320  tgqioo  18358  re2ndc  18359  xrsdsre  18368  xrsmopn  18370  metdcn2  18396  metdscn2  18413  oprpiece1res2  18503  bndth  18509  pcoass  18575  ovolfioo  18880  ovolficc  18881  ovolficcss  18882  ovollb  18891  ovolunlem1a  18908  ovolunlem1  18909  ovoliunlem1  18914  ovoliun  18917  ovolicc2lem4  18932  ovolicc2  18934  voliunlem2  18961  voliunlem3  18962  ovolfs2  18979  uniiccdif  18986  uniioovol  18987  uniiccvol  18988  uniioombllem2  18991  uniioombllem3a  18992  uniioombllem3  18993  uniioombllem4  18994  uniioombllem5  18995  uniioombl  18997  dyadmbllem  19007  opnmbllem  19009  opnmblALT  19011  vitalilem4  19019  mbfimaopnlem  19063  itg2le  19147  itg2seq  19150  dvfsumrlim  19431  itgsubst  19449  mdegleb  19503  mdeglt  19504  mdegldg  19505  mdegxrcl  19506  mdegcl  19508  mdegaddle  19513  mdegmullem  19517  deg1mul3le  19555  ig1pdvds  19615  aannenlem2  19762  taylfval  19791  radcnvcl  19846  radcnvlt1  19847  radcnvle  19849  sincosq4sgn  19922  tanabsge  19927  sinq12gt0  19928  cosq14gt0  19931  tanord1  19952  tanregt0  19954  ellogrn  19970  argregt0  20017  argimgt0  20019  argimlt0  20020  dvloglem  20048  asinneg  20235  asinsinlem  20240  acoscos  20242  reasinsin  20245  atanlogsublem  20264  atanbndlem  20274  atanbnd  20275  atan1  20277  xrlimcnp  20316  scvxcvx  20333  basellem4  20374  pntibndlem2  20793  padicabvf  20833  padicabvcxp  20834  nmoxr  21399  nmooge0  21400  nmoolb  21404  nmoubi  21405  nmlno0lem  21426  nmopxr  22501  nmfnxr  22514  nmoplb  22542  nmopub  22543  nmfnlb  22559  nmfnleub  22560  nmlnop0iALT  22630  nmopun  22649  branmfn  22740  pjnmopi  22783  xlt2addrd  23270  xreceu  23320  rexdiv  23324  xrsmulgzz  23342  xrge0iifcnv  23388  esumcst  23631  dstrvprob  23903  umgrafi  24158  prodmolem2a  24437  itg2addnc  25319  prdsbnd  25665  rrnequiv  25707  hbtlem2  26476
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-6 1720  ax-7 1725  ax-11 1732  ax-12 1897  ax-ext 2297
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1533  df-nf 1536  df-sb 1640  df-clab 2303  df-cleq 2309  df-clel 2312  df-nfc 2441  df-v 2824  df-un 3191  df-in 3193  df-ss 3200  df-xr 8916
  Copyright terms: Public domain W3C validator