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

Theorem ressxr 8892
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 3351 . 2  |-  RR  C_  ( RR  u.  {  +oo , 
-oo } )
2 df-xr 8887 . 2  |-  RR*  =  ( RR  u.  {  +oo , 
-oo } )
31, 2sseqtr4i 3224 1  |-  RR  C_  RR*
Colors of variables: wff set class
Syntax hints:    u. cun 3163    C_ wss 3165   {cpr 3654   RRcr 8752    +oocpnf 8880    -oocmnf 8881   RR*cxr 8882
This theorem is referenced by:  rexr  8893  0xr  8894  rexrd  8897  ltrelxr  8902  supxrre  10662  supxrbnd  10663  supxrgtmnf  10664  supxrre1  10665  supxrre2  10666  infmxrre  10670  iooval2  10705  fzval2  10801  uzsup  10983  hashxrcl  11367  seqcoll  11417  limsupval2  11970  limsupgre  11971  limsupbnd2  11973  rlimuni  12040  rlimcld2  12068  rlimno1  12143  isercolllem2  12155  isercoll  12157  caucvgrlem  12161  summolem2a  12204  tanhbnd  12457  ramtlecl  13063  ramxrcl  13080  ismet2  17914  prdsmet  17950  qtopbas  18284  tgqioo  18322  re2ndc  18323  xrsdsre  18332  xrsmopn  18334  metdcn2  18360  metdscn2  18377  oprpiece1res2  18466  bndth  18472  pcoass  18538  ovolfioo  18843  ovolficc  18844  ovolficcss  18845  ovollb  18854  ovolunlem1a  18871  ovolunlem1  18872  ovoliunlem1  18877  ovoliun  18880  ovolicc2lem4  18895  ovolicc2  18897  voliunlem2  18924  voliunlem3  18925  ovolfs2  18942  uniiccdif  18949  uniioovol  18950  uniiccvol  18951  uniioombllem2  18954  uniioombllem3a  18955  uniioombllem3  18956  uniioombllem4  18957  uniioombllem5  18958  uniioombl  18960  dyadmbllem  18970  opnmbllem  18972  opnmblALT  18974  vitalilem4  18982  mbfimaopnlem  19026  itg2le  19110  itg2seq  19113  dvfsumrlim  19394  itgsubst  19412  mdegleb  19466  mdeglt  19467  mdegldg  19468  mdegxrcl  19469  mdegcl  19471  mdegaddle  19476  mdegmullem  19480  deg1mul3le  19518  ig1pdvds  19578  aannenlem2  19725  taylfval  19754  radcnvcl  19809  radcnvlt1  19810  radcnvle  19812  sincosq4sgn  19885  tanabsge  19890  sinq12gt0  19891  cosq14gt0  19894  tanord1  19915  tanregt0  19917  ellogrn  19933  argregt0  19980  argimgt0  19982  argimlt0  19983  dvloglem  20011  asinneg  20198  asinsinlem  20203  acoscos  20205  reasinsin  20208  atanlogsublem  20227  atanbndlem  20237  atanbnd  20238  atan1  20240  xrlimcnp  20279  scvxcvx  20296  basellem4  20337  pntibndlem2  20756  padicabvf  20796  padicabvcxp  20797  nmoxr  21360  nmooge0  21361  nmoolb  21365  nmoubi  21366  nmlno0lem  21387  nmopxr  22462  nmfnxr  22475  nmoplb  22503  nmopub  22504  nmfnlb  22520  nmfnleub  22521  nmlnop0iALT  22591  nmopun  22610  branmfn  22701  pjnmopi  22744  xreceu  23121  rexdiv  23125  xlt2addrd  23268  xrsmulgzz  23322  xrge0iifcnv  23330  esumcst  23451  dstrvprob  23687  umgrafi  23889  prodmolem2a  24157  itg2addnc  25004  basexre  25624  altretop  25702  prdsbnd  26619  rrnequiv  26661  hbtlem2  27430
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-un 3170  df-in 3172  df-ss 3179  df-xr 8887
  Copyright terms: Public domain W3C validator