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

Theorem ioossre 13020
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 12989 . 2 (𝑥 ∈ (𝐴(,)𝐵) → 𝑥 ∈ ℝ)
21ssriv 3919 1 (𝐴(,)𝐵) ⊆ ℝ
Colors of variables: wff setvar class
Syntax hints:  wss 3880  (class class class)co 7231  cr 10752  (,)cioo 12959
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2159  ax-12 2176  ax-ext 2709  ax-sep 5206  ax-nul 5213  ax-pow 5272  ax-pr 5336  ax-un 7541  ax-cnex 10809  ax-resscn 10810  ax-pre-lttri 10827  ax-pre-lttrn 10828
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2072  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3067  df-rex 3068  df-rab 3071  df-v 3422  df-sbc 3709  df-csb 3826  df-dif 3883  df-un 3885  df-in 3887  df-ss 3897  df-nul 4252  df-if 4454  df-pw 4529  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4834  df-iun 4920  df-br 5068  df-opab 5130  df-mpt 5150  df-id 5469  df-po 5482  df-so 5483  df-xp 5571  df-rel 5572  df-cnv 5573  df-co 5574  df-dm 5575  df-rn 5576  df-res 5577  df-ima 5578  df-iota 6355  df-fun 6399  df-fn 6400  df-f 6401  df-f1 6402  df-fo 6403  df-f1o 6404  df-fv 6405  df-ov 7234  df-oprab 7235  df-mpo 7236  df-1st 7779  df-2nd 7780  df-er 8411  df-en 8647  df-dom 8648  df-sdom 8649  df-pnf 10893  df-mnf 10894  df-xr 10895  df-ltxr 10896  df-le 10897  df-ioo 12963
This theorem is referenced by:  ioosscn  13021  ioof  13059  difreicc  13096  icopnfcld  23689  ioombl1  24483  ioorcl2  24493  uniioombllem2  24504  uniioombllem3a  24505  uniioombllem3  24506  uniioombllem4  24507  uniioombllem6  24509  ismbf3d  24575  itgsplitioo  24759  ditgeq3  24771  dvmptresicc  24837  dvferm1lem  24905  dvferm2lem  24907  dvferm  24909  dvlip  24914  dvlipcn  24915  dvle  24928  dvivthlem1  24929  dvivth  24931  lhop1lem  24934  lhop1  24935  lhop2  24936  lhop  24937  dvfsumle  24942  dvfsumge  24943  dvfsumlem1  24947  dvfsumlem2  24948  dvfsumlem3  24949  dvfsumlem4  24950  dvfsumrlimge0  24951  dvfsumrlim  24952  dvfsumrlim2  24953  dvfsum2  24955  ftc1a  24958  ftc1cn  24964  ftc2  24965  itgsubstlem  24969  itgsubst  24970  itgpowd  24971  efcvx  25365  pige3ALT  25433  tanord  25451  divlogrlim  25547  logccv  25575  atantan  25830  amgmlem  25896  vmalogdivsum2  26443  2vmadivsumlem  26445  chpdifbndlem1  26458  selberg3lem1  26462  selberg4lem1  26465  selberg4  26466  selberg3r  26474  selberg4r  26475  selberg34r  26476  pntrlog2bndlem2  26483  pntrlog2bndlem3  26484  pntrlog2bndlem4  26485  pntrlog2bndlem5  26486  pntrlog2bndlem6  26488  pntrlog2bnd  26489  pntpbnd1a  26490  pntpbnd1  26491  pntpbnd2  26492  pntibndlem2a  26495  pntibndlem2  26496  pntibndlem3  26497  pntlemd  26499  pnt  26519  padicabv  26535  cnre2csqima  31599  ftc2re  32314  fdvposlt  32315  fdvposle  32317  itgexpif  32322  circlemeth  32356  circlemethnat  32357  circlevma  32358  circlemethhgt  32359  ioosconn  32945  iccllysconn  32948  itg2gt0cn  35595  itggt0cn  35610  ftc1cnnclem  35611  ftc1cnnc  35612  ftc1anclem8  35620  ftc2nc  35622  dvreasin  35626  dvreacos  35627  areacirclem1  35628  areacirc  35633  aks4d1p1p6  39840  aks4d1p1p5  39842  ioontr  42752  iooshift  42763  ioonct  42778  iooiinicc  42783  icomnfinre  42793  iooiinioc  42797  islptre  42863  lptioo2  42875  lptioo1  42876  limcresiooub  42886  limcresioolb  42887  limcleqr  42888  lptioo2cn  42889  lptioo1cn  42890  limclner  42895  limclr  42899  icccncfext  43131  cncfiooicclem1  43137  dvresioo  43165  dvbdfbdioolem1  43172  dvbdfbdioolem2  43173  ioodvbdlimc1lem1  43175  ioodvbdlimc1lem2  43176  ioodvbdlimc2lem  43178  itgsin0pilem1  43194  itgcoscmulx  43213  itgiccshift  43224  itgperiod  43225  itgsbtaddcnst  43226  dirkercncflem2  43348  dirkercncflem3  43349  dirkercncflem4  43350  fourierdlem16  43367  fourierdlem21  43372  fourierdlem22  43373  fourierdlem28  43379  fourierdlem48  43398  fourierdlem49  43399  fourierdlem50  43400  fourierdlem56  43406  fourierdlem57  43407  fourierdlem59  43409  fourierdlem60  43410  fourierdlem61  43411  fourierdlem65  43415  fourierdlem72  43422  fourierdlem74  43424  fourierdlem75  43425  fourierdlem76  43426  fourierdlem80  43430  fourierdlem81  43431  fourierdlem83  43433  fourierdlem84  43434  fourierdlem85  43435  fourierdlem88  43438  fourierdlem89  43439  fourierdlem90  43440  fourierdlem91  43441  fourierdlem92  43442  fourierdlem94  43444  fourierdlem95  43445  fourierdlem97  43447  fourierdlem101  43451  fourierdlem103  43453  fourierdlem104  43454  fourierdlem111  43461  fourierdlem112  43462  fourierdlem113  43463  fouriersw  43475  fouriercn  43476  ioorrnopnlem  43548  hspdifhsp  43857  hspmbllem2  43868  hspmbl  43870  iunhoiioolem  43916  smfresal  44022  smfpimbor1lem1  44032
  Copyright terms: Public domain W3C validator