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

Theorem ioossre 13332
Description: An open interval is a set of reals. (Contributed by NM, 31-May-2007.)
Assertion
Ref Expression
ioossre (𝐴(,)𝐵) ⊆ ℝ

Proof of Theorem ioossre
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 elioore 13301 . 2 (𝑥 ∈ (𝐴(,)𝐵) → 𝑥 ∈ ℝ)
21ssriv 3953 1 (𝐴(,)𝐵) ⊆ ℝ
Colors of variables: wff setvar class
Syntax hints:  wss 3915  (class class class)co 7362  cr 11057  (,)cioo 13271
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677  ax-cnex 11114  ax-resscn 11115  ax-pre-lttri 11132  ax-pre-lttrn 11133
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3066  df-rex 3075  df-rab 3411  df-v 3450  df-sbc 3745  df-csb 3861  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-iun 4961  df-br 5111  df-opab 5173  df-mpt 5194  df-id 5536  df-po 5550  df-so 5551  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-ov 7365  df-oprab 7366  df-mpo 7367  df-1st 7926  df-2nd 7927  df-er 8655  df-en 8891  df-dom 8892  df-sdom 8893  df-pnf 11198  df-mnf 11199  df-xr 11200  df-ltxr 11201  df-le 11202  df-ioo 13275
This theorem is referenced by:  ioosscn  13333  ioof  13371  difreicc  13408  icopnfcld  24147  ioombl1  24942  ioorcl2  24952  uniioombllem2  24963  uniioombllem3a  24964  uniioombllem3  24965  uniioombllem4  24966  uniioombllem6  24968  ismbf3d  25034  itgsplitioo  25218  ditgeq3  25230  dvmptresicc  25296  dvferm1lem  25364  dvferm2lem  25366  dvferm  25368  dvlip  25373  dvlipcn  25374  dvle  25387  dvivthlem1  25388  dvivth  25390  lhop1lem  25393  lhop1  25394  lhop2  25395  lhop  25396  dvfsumle  25401  dvfsumge  25402  dvfsumlem1  25406  dvfsumlem2  25407  dvfsumlem3  25408  dvfsumlem4  25409  dvfsumrlimge0  25410  dvfsumrlim  25411  dvfsumrlim2  25412  dvfsum2  25414  ftc1a  25417  ftc1cn  25423  ftc2  25424  itgsubstlem  25428  itgsubst  25429  itgpowd  25430  efcvx  25824  pige3ALT  25892  tanord  25910  divlogrlim  26006  logccv  26034  atantan  26289  amgmlem  26355  vmalogdivsum2  26902  2vmadivsumlem  26904  chpdifbndlem1  26917  selberg3lem1  26921  selberg4lem1  26924  selberg4  26925  selberg3r  26933  selberg4r  26934  selberg34r  26935  pntrlog2bndlem2  26942  pntrlog2bndlem3  26943  pntrlog2bndlem4  26944  pntrlog2bndlem5  26945  pntrlog2bndlem6  26947  pntrlog2bnd  26948  pntpbnd1a  26949  pntpbnd1  26950  pntpbnd2  26951  pntibndlem2a  26954  pntibndlem2  26955  pntibndlem3  26956  pntlemd  26958  pnt  26978  padicabv  26994  cnre2csqima  32532  ftc2re  33251  fdvposlt  33252  fdvposle  33254  itgexpif  33259  circlemeth  33293  circlemethnat  33294  circlevma  33295  circlemethhgt  33296  ioosconn  33881  iccllysconn  33884  itg2gt0cn  36162  itggt0cn  36177  ftc1cnnclem  36178  ftc1cnnc  36179  ftc1anclem8  36187  ftc2nc  36189  dvreasin  36193  dvreacos  36194  areacirclem1  36195  areacirc  36200  aks4d1p1p6  40559  aks4d1p1p5  40561  ioontr  43823  iooshift  43834  ioonct  43849  iooiinicc  43854  icomnfinre  43864  iooiinioc  43868  islptre  43934  lptioo2  43946  lptioo1  43947  limcresiooub  43957  limcresioolb  43958  limcleqr  43959  lptioo2cn  43960  lptioo1cn  43961  limclner  43966  limclr  43970  icccncfext  44202  cncfiooicclem1  44208  dvresioo  44236  dvbdfbdioolem1  44243  dvbdfbdioolem2  44244  ioodvbdlimc1lem1  44246  ioodvbdlimc1lem2  44247  ioodvbdlimc2lem  44249  itgsin0pilem1  44265  itgcoscmulx  44284  itgiccshift  44295  itgperiod  44296  itgsbtaddcnst  44297  dirkercncflem2  44419  dirkercncflem3  44420  dirkercncflem4  44421  fourierdlem16  44438  fourierdlem21  44443  fourierdlem22  44444  fourierdlem28  44450  fourierdlem48  44469  fourierdlem49  44470  fourierdlem50  44471  fourierdlem56  44477  fourierdlem57  44478  fourierdlem59  44480  fourierdlem60  44481  fourierdlem61  44482  fourierdlem65  44486  fourierdlem72  44493  fourierdlem74  44495  fourierdlem75  44496  fourierdlem76  44497  fourierdlem80  44501  fourierdlem81  44502  fourierdlem83  44504  fourierdlem84  44505  fourierdlem85  44506  fourierdlem88  44509  fourierdlem89  44510  fourierdlem90  44511  fourierdlem91  44512  fourierdlem92  44513  fourierdlem94  44515  fourierdlem95  44516  fourierdlem97  44518  fourierdlem101  44522  fourierdlem103  44524  fourierdlem104  44525  fourierdlem111  44532  fourierdlem112  44533  fourierdlem113  44534  fouriersw  44546  fouriercn  44547  ioorrnopnlem  44619  hspdifhsp  44931  hspmbllem2  44942  hspmbl  44944  iunhoiioolem  44990  smfresal  45103  smfpimbor1lem1  45113
  Copyright terms: Public domain W3C validator