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

Theorem ressxr 9658
Description: The standard reals are a subset of the extended reals. (Contributed by NM, 14-Oct-2005.)
Assertion
Ref Expression
ressxr

Proof of Theorem ressxr
StepHypRef Expression
1 ssun1 3666 . 2
2 df-xr 9653 . 2
31, 2sseqtr4i 3536 1
Colors of variables: wff setvar class
Syntax hints:  u.cun 3473  C_wss 3475  {cpr 4031   cr 9512   cpnf 9646   cmnf 9647   cxr 9648
This theorem is referenced by:  rexpssxrxp  9659  rexr  9660  0xr  9661  rexrd  9664  ltrelxr  9669  supxrre  11548  supxrbnd  11549  supxrgtmnf  11550  supxrre1  11551  supxrre2  11552  infmxrre  11556  iooval2  11591  fzval2  11704  uzsup  11990  hashxrcl  12429  seqcoll  12512  limsupval2  13303  limsupgre  13304  limsupbnd2  13306  rlimuni  13373  rlimcld2  13401  rlimno1  13476  isercolllem2  13488  isercoll  13490  caucvgrlem  13495  summolem2a  13537  prodmolem2a  13741  ramtlecl  14518  ramxrcl  14535  ismet2  20836  prdsmet  20873  qtopbas  21266  tgqioo  21305  re2ndc  21306  xrsmopn  21317  metdcn2  21344  metdscn2  21361  bndth  21458  ovolunlem1a  21907  ovolunlem1  21908  ovoliunlem1  21913  ovoliun  21916  ovolicc2lem4  21931  voliunlem2  21961  voliunlem3  21962  opnmblALT  22012  vitalilem4  22020  mbfimaopnlem  22062  itg2le  22146  itg2seq  22149  dvfsumrlim  22432  itgsubst  22450  mdegleb  22464  mdeglt  22465  mdegldg  22466  mdegxrcl  22467  mdegcl  22469  mdegaddle  22474  mdegmullem  22478  deg1mul3le  22517  ig1pdvds  22577  aannenlem2  22725  taylfval  22754  radcnvcl  22812  radcnvlt1  22813  radcnvle  22815  xrlimcnp  23298  nmoxr  25681  nmooge0  25682  nmoolb  25686  nmoubi  25687  nmlno0lem  25708  nmopxr  26785  nmfnxr  26798  nmoplb  26826  nmopub  26827  nmfnlb  26843  nmfnleub  26844  nmlnop0iALT  26914  nmopun  26933  branmfn  27024  pjnmopi  27067  xlt2addrd  27578  xreceu  27618  rexdiv  27622  xrsmulgzz  27666  esumcst  28071  mblfinlem2  30052  itg2addnc  30069  prdsbnd  30289  rrnequiv  30331  hbtlem2  31073  binomcxplemdvbinom  31258  binomcxplemcvg  31259  binomcxplemnotnn0  31261  limsupre  31647  fourierdlem52  31941  fourierdlem103  31992  fourierdlem104  31993  etransclem48  32065
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-un 3480  df-in 3482  df-ss 3489  df-xr 9653
  Copyright terms: Public domain W3C validator