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

Theorem ressxr 9055
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 3446 . 2  |-  RR  C_  ( RR  u.  {  +oo , 
-oo } )
2 df-xr 9050 . 2  |-  RR*  =  ( RR  u.  {  +oo , 
-oo } )
31, 2sseqtr4i 3317 1  |-  RR  C_  RR*
Colors of variables: wff set class
Syntax hints:    u. cun 3254    C_ wss 3256   {cpr 3751   RRcr 8915    +oocpnf 9043    -oocmnf 9044   RR*cxr 9045
This theorem is referenced by:  rexr  9056  0xr  9057  rexrd  9060  ltrelxr  9065  supxrre  10831  supxrbnd  10832  supxrgtmnf  10833  supxrre1  10834  supxrre2  10835  infmxrre  10839  iooval2  10874  fzval2  10971  uzsup  11164  hashxrcl  11560  seqcoll  11632  limsupval2  12194  limsupgre  12195  limsupbnd2  12197  rlimuni  12264  rlimcld2  12292  rlimno1  12367  isercolllem2  12379  isercoll  12381  caucvgrlem  12386  summolem2a  12429  ramtlecl  13288  ramxrcl  13305  ismet2  18265  prdsmet  18301  qtopbas  18657  tgqioo  18695  re2ndc  18696  xrsdsre  18705  xrsmopn  18707  metdcn2  18734  metdscn2  18751  bndth  18847  ovolfioo  19224  ovolficc  19225  ovolficcss  19226  ovollb  19235  ovolunlem1a  19252  ovolunlem1  19253  ovoliunlem1  19258  ovoliun  19261  ovolicc2lem4  19276  ovolicc2  19278  voliunlem2  19305  voliunlem3  19306  ovolfs2  19323  uniiccdif  19330  uniioovol  19331  uniiccvol  19332  uniioombllem2  19335  uniioombllem3a  19336  uniioombllem3  19337  uniioombllem4  19338  uniioombllem5  19339  uniioombl  19341  dyadmbllem  19351  opnmbllem  19353  opnmblALT  19355  vitalilem4  19363  mbfimaopnlem  19407  itg2le  19491  itg2seq  19494  dvfsumrlim  19775  itgsubst  19793  mdegleb  19847  mdeglt  19848  mdegldg  19849  mdegxrcl  19850  mdegcl  19852  mdegaddle  19857  mdegmullem  19861  deg1mul3le  19899  ig1pdvds  19959  aannenlem2  20106  taylfval  20135  radcnvcl  20193  radcnvlt1  20194  radcnvle  20196  xrlimcnp  20667  nmoxr  22108  nmooge0  22109  nmoolb  22113  nmoubi  22114  nmlno0lem  22135  nmopxr  23210  nmfnxr  23223  nmoplb  23251  nmopub  23252  nmfnlb  23268  nmfnleub  23269  nmlnop0iALT  23339  nmopun  23358  branmfn  23449  pjnmopi  23492  xlt2addrd  23953  xreceu  23999  rexdiv  24003  xrsmulgzz  24026  esumcst  24244  prodmolem2a  25032  itg2addnc  25952  prdsbnd  26186  rrnequiv  26228  hbtlem2  26990
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 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2361
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 2367  df-cleq 2373  df-clel 2376  df-nfc 2505  df-v 2894  df-un 3261  df-in 3263  df-ss 3270  df-xr 9050
  Copyright terms: Public domain W3C validator