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

Theorem ioossre 12440
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 12410 . 2 (𝑥 ∈ (𝐴(,)𝐵) → 𝑥 ∈ ℝ)
21ssriv 3756 1 (𝐴(,)𝐵) ⊆ ℝ
Colors of variables: wff setvar class
Syntax hints:  wss 3723  (class class class)co 6793  cr 10137  (,)cioo 12380
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7096  ax-cnex 10194  ax-resscn 10195  ax-pre-lttri 10212  ax-pre-lttrn 10213
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3or 1072  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-nel 3047  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-op 4323  df-uni 4575  df-iun 4656  df-br 4787  df-opab 4847  df-mpt 4864  df-id 5157  df-po 5170  df-so 5171  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-fo 6037  df-f1o 6038  df-fv 6039  df-ov 6796  df-oprab 6797  df-mpt2 6798  df-1st 7315  df-2nd 7316  df-er 7896  df-en 8110  df-dom 8111  df-sdom 8112  df-pnf 10278  df-mnf 10279  df-xr 10280  df-ltxr 10281  df-le 10282  df-ioo 12384
This theorem is referenced by:  ioof  12477  difreicc  12511  icopnfcld  22791  ioombl1  23550  ioorcl2  23560  uniioombllem2  23571  uniioombllem3a  23572  uniioombllem3  23573  uniioombllem4  23574  uniioombllem6  23576  ismbf3d  23641  itgsplitioo  23824  ditgeq3  23834  dvferm1lem  23967  dvferm2lem  23969  dvferm  23971  dvlip  23976  dvlipcn  23977  dvle  23990  dvivthlem1  23991  dvivth  23993  lhop1lem  23996  lhop1  23997  lhop2  23998  lhop  23999  dvfsumle  24004  dvfsumge  24005  dvfsumlem1  24009  dvfsumlem2  24010  dvfsumlem3  24011  dvfsumlem4  24012  dvfsumrlimge0  24013  dvfsumrlim  24014  dvfsumrlim2  24015  dvfsum2  24017  ftc1a  24020  ftc1cn  24026  ftc2  24027  itgsubstlem  24031  itgsubst  24032  efcvx  24423  pige3  24490  tanord  24505  divlogrlim  24602  logccv  24630  atantan  24871  amgmlem  24937  vmalogdivsum2  25448  2vmadivsumlem  25450  chpdifbndlem1  25463  selberg3lem1  25467  selberg4lem1  25470  selberg4  25471  selberg3r  25479  selberg4r  25480  selberg34r  25481  pntrlog2bndlem2  25488  pntrlog2bndlem3  25489  pntrlog2bndlem4  25490  pntrlog2bndlem5  25491  pntrlog2bndlem6  25493  pntrlog2bnd  25494  pntpbnd1a  25495  pntpbnd1  25496  pntpbnd2  25497  pntibndlem2a  25500  pntibndlem2  25501  pntibndlem3  25502  pntlemd  25504  pnt  25524  padicabv  25540  cnre2csqima  30297  ftc2re  31016  fdvposlt  31017  fdvposle  31019  itgexpif  31024  circlemeth  31058  circlemethnat  31059  circlevma  31060  circlemethhgt  31061  ioosconn  31567  iccllysconn  31570  itg2gt0cn  33797  itggt0cn  33814  ftc1cnnclem  33815  ftc1cnnc  33816  ftc1anclem8  33824  ftc2nc  33826  dvreasin  33830  dvreacos  33831  areacirclem1  33832  areacirc  33837  itgpowd  38326  ioosscn  40237  ioontr  40256  iooshift  40267  ioonct  40282  iooiinicc  40287  icomnfinre  40297  iooiinioc  40301  islptre  40369  lptioo2  40381  lptioo1  40382  limcresiooub  40392  limcresioolb  40393  limcleqr  40394  lptioo2cn  40395  lptioo1cn  40396  limclner  40401  limclr  40405  icccncfext  40618  cncfiooicclem1  40624  dvmptresicc  40652  dvresioo  40654  dvbdfbdioolem1  40661  dvbdfbdioolem2  40662  ioodvbdlimc1lem1  40664  ioodvbdlimc1lem2  40665  ioodvbdlimc2lem  40667  itgsin0pilem1  40683  itgcoscmulx  40702  itgiccshift  40713  itgperiod  40714  itgsbtaddcnst  40715  dirkercncflem2  40838  dirkercncflem3  40839  dirkercncflem4  40840  fourierdlem16  40857  fourierdlem21  40862  fourierdlem22  40863  fourierdlem28  40869  fourierdlem48  40888  fourierdlem49  40889  fourierdlem50  40890  fourierdlem56  40896  fourierdlem57  40897  fourierdlem59  40899  fourierdlem60  40900  fourierdlem61  40901  fourierdlem65  40905  fourierdlem72  40912  fourierdlem74  40914  fourierdlem75  40915  fourierdlem76  40916  fourierdlem80  40920  fourierdlem81  40921  fourierdlem83  40923  fourierdlem84  40924  fourierdlem85  40925  fourierdlem88  40928  fourierdlem89  40929  fourierdlem90  40930  fourierdlem91  40931  fourierdlem92  40932  fourierdlem94  40934  fourierdlem95  40935  fourierdlem97  40937  fourierdlem101  40941  fourierdlem103  40943  fourierdlem104  40944  fourierdlem111  40951  fourierdlem112  40952  fourierdlem113  40953  fouriersw  40965  fouriercn  40966  ioorrnopnlem  41041  hspdifhsp  41350  hspmbllem2  41361  hspmbl  41363  iunhoiioolem  41409  smfresal  41515  smfpimbor1lem1  41525
  Copyright terms: Public domain W3C validator