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

Theorem ioossre 11362
Description: An open interval is a set of reals. (Contributed by NM, 31-May-2007.)
Assertion
Ref Expression
ioossre  |-  ( A (,) B )  C_  RR

Proof of Theorem ioossre
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 elioore 11335 . 2  |-  ( x  e.  ( A (,) B )  ->  x  e.  RR )
21ssriv 3365 1  |-  ( A (,) B )  C_  RR
Colors of variables: wff setvar class
Syntax hints:    C_ wss 3333  (class class class)co 6096   RRcr 9286   (,)cioo 11305
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4418  ax-nul 4426  ax-pow 4475  ax-pr 4536  ax-un 6377  ax-cnex 9343  ax-resscn 9344  ax-pre-lttri 9361  ax-pre-lttrn 9362
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2573  df-ne 2613  df-nel 2614  df-ral 2725  df-rex 2726  df-rab 2729  df-v 2979  df-sbc 3192  df-csb 3294  df-dif 3336  df-un 3338  df-in 3340  df-ss 3347  df-nul 3643  df-if 3797  df-pw 3867  df-sn 3883  df-pr 3885  df-op 3889  df-uni 4097  df-iun 4178  df-br 4298  df-opab 4356  df-mpt 4357  df-id 4641  df-po 4646  df-so 4647  df-xp 4851  df-rel 4852  df-cnv 4853  df-co 4854  df-dm 4855  df-rn 4856  df-res 4857  df-ima 4858  df-iota 5386  df-fun 5425  df-fn 5426  df-f 5427  df-f1 5428  df-fo 5429  df-f1o 5430  df-fv 5431  df-ov 6099  df-oprab 6100  df-mpt2 6101  df-1st 6582  df-2nd 6583  df-er 7106  df-en 7316  df-dom 7317  df-sdom 7318  df-pnf 9425  df-mnf 9426  df-xr 9427  df-ltxr 9428  df-le 9429  df-ioo 11309
This theorem is referenced by:  ioof  11392  difreicc  11422  icopnfcld  20352  ioombl1  21048  ioorcl2  21057  uniioombllem2  21068  uniioombllem3a  21069  uniioombllem3  21070  uniioombllem4  21071  uniioombllem6  21073  ismbf3d  21137  itgsplitioo  21320  ditgeq3  21330  dvferm1lem  21461  dvferm2lem  21463  dvferm  21465  dvlip  21470  dvlipcn  21471  dvle  21484  dvivthlem1  21485  dvivth  21487  lhop1lem  21490  lhop1  21491  lhop2  21492  lhop  21493  dvfsumle  21498  dvfsumge  21499  dvfsumlem1  21503  dvfsumlem2  21504  dvfsumlem3  21505  dvfsumlem4  21506  dvfsumrlimge0  21507  dvfsumrlim  21508  dvfsumrlim2  21509  dvfsum2  21511  ftc1a  21514  ftc1cn  21520  ftc2  21521  itgsubstlem  21525  itgsubst  21526  efcvx  21919  pige3  21984  tanord  21999  divlogrlim  22085  logccv  22113  atantan  22323  amgmlem  22388  vmalogdivsum2  22792  2vmadivsumlem  22794  chpdifbndlem1  22807  selberg3lem1  22811  selberg4lem1  22814  selberg4  22815  selberg3r  22823  selberg4r  22824  selberg34r  22825  pntrlog2bndlem2  22832  pntrlog2bndlem3  22833  pntrlog2bndlem4  22834  pntrlog2bndlem5  22835  pntrlog2bndlem6  22837  pntrlog2bnd  22838  pntpbnd1a  22839  pntpbnd1  22840  pntpbnd2  22841  pntibndlem2a  22844  pntibndlem2  22845  pntibndlem3  22846  pntlemd  22848  pnt  22868  padicabv  22884  cnre2csqima  26346  iooscon  27141  iccllyscon  27144  itg2gt0cn  28452  itggt0cn  28469  ftc1cnnclem  28470  ftc1cnnc  28471  ftc1anclem8  28479  ftc2nc  28481  dvreasin  28487  dvreacos  28488  areacirclem1  28489  areacirc  28494  itgpowd  29595  itgsin0pilem1  29795  itgsinexplem1  29799  itgsinexp  29800  wallispilem2  29866
  Copyright terms: Public domain W3C validator