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

Theorem ressxr 9119
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 3502 . 2  |-  RR  C_  ( RR  u.  {  +oo , 
-oo } )
2 df-xr 9114 . 2  |-  RR*  =  ( RR  u.  {  +oo , 
-oo } )
31, 2sseqtr4i 3373 1  |-  RR  C_  RR*
Colors of variables: wff set class
Syntax hints:    u. cun 3310    C_ wss 3312   {cpr 3807   RRcr 8979    +oocpnf 9107    -oocmnf 9108   RR*cxr 9109
This theorem is referenced by:  rexr  9120  0xr  9121  rexrd  9124  ltrelxr  9129  supxrre  10896  supxrbnd  10897  supxrgtmnf  10898  supxrre1  10899  supxrre2  10900  infmxrre  10904  iooval2  10939  fzval2  11036  uzsup  11234  hashxrcl  11630  seqcoll  11702  limsupval2  12264  limsupgre  12265  limsupbnd2  12267  rlimuni  12334  rlimcld2  12362  rlimno1  12437  isercolllem2  12449  isercoll  12451  caucvgrlem  12456  summolem2a  12499  ramtlecl  13358  ramxrcl  13375  ismet2  18353  prdsmet  18390  qtopbas  18783  tgqioo  18821  re2ndc  18822  xrsdsre  18831  xrsmopn  18833  metdcn2  18860  metdscn2  18877  bndth  18973  ovolfioo  19354  ovolficc  19355  ovolficcss  19356  ovollb  19365  ovolunlem1a  19382  ovolunlem1  19383  ovoliunlem1  19388  ovoliun  19391  ovolicc2lem4  19406  ovolicc2  19408  voliunlem2  19435  voliunlem3  19436  ovolfs2  19453  uniiccdif  19460  uniioovol  19461  uniiccvol  19462  uniioombllem2  19465  uniioombllem3a  19466  uniioombllem3  19467  uniioombllem4  19468  uniioombllem5  19469  uniioombl  19471  dyadmbllem  19481  opnmbllem  19483  opnmblALT  19485  vitalilem4  19493  mbfimaopnlem  19537  itg2le  19621  itg2seq  19624  dvfsumrlim  19905  itgsubst  19923  mdegleb  19977  mdeglt  19978  mdegldg  19979  mdegxrcl  19980  mdegcl  19982  mdegaddle  19987  mdegmullem  19991  deg1mul3le  20029  ig1pdvds  20089  aannenlem2  20236  taylfval  20265  radcnvcl  20323  radcnvlt1  20324  radcnvle  20326  xrlimcnp  20797  nmoxr  22257  nmooge0  22258  nmoolb  22262  nmoubi  22263  nmlno0lem  22284  nmopxr  23359  nmfnxr  23372  nmoplb  23400  nmopub  23401  nmfnlb  23417  nmfnleub  23418  nmlnop0iALT  23488  nmopun  23507  branmfn  23598  pjnmopi  23641  xlt2addrd  24114  xreceu  24158  rexdiv  24162  xrsmulgzz  24190  esumcst  24445  prodmolem2a  25250  mblfinlem  26207  itg2addnc  26222  prdsbnd  26456  rrnequiv  26498  hbtlem2  27260
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-v 2950  df-un 3317  df-in 3319  df-ss 3326  df-xr 9114
  Copyright terms: Public domain W3C validator