Theorem ioossre 13149

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.

Step	Hyp	Ref	Expression
1		elioore 13118	. 2 ⊢ (𝑥 ∈ (𝐴(,)𝐵) → 𝑥 ∈ ℝ)
2	1	ssriv 3926	1 ⊢ (𝐴(,)𝐵) ⊆ ℝ

Syntax hints:   ⊆ wss 3888  (class class class)co 7284  ℝcr 10879  (,)cioo 13088

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 2710  ax-sep 5224  ax-nul 5231  ax-pow 5289  ax-pr 5353  ax-un 7597  ax-cnex 10936  ax-resscn 10937  ax-pre-lttri 10954  ax-pre-lttrn 10955

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3435  df-sbc 3718  df-csb 3834  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-pw 4536  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-iun 4927  df-br 5076  df-opab 5138  df-mpt 5159  df-id 5490  df-po 5504  df-so 5505  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-iota 6395  df-fun 6439  df-fn 6440  df-f 6441  df-f1 6442  df-fo 6443  df-f1o 6444  df-fv 6445  df-ov 7287  df-oprab 7288  df-mpo 7289  df-1st 7840  df-2nd 7841  df-er 8507  df-en 8743  df-dom 8744  df-sdom 8745  df-pnf 11020  df-mnf 11021  df-xr 11022  df-ltxr 11023  df-le 11024  df-ioo 13092

This theorem is referenced by:  ioosscn  13150  ioof  13188  difreicc  13225  icopnfcld  23940  ioombl1  24735  ioorcl2  24745  uniioombllem2  24756  uniioombllem3a  24757  uniioombllem3  24758  uniioombllem4  24759  uniioombllem6  24761  ismbf3d  24827  itgsplitioo  25011  ditgeq3  25023  dvmptresicc  25089  dvferm1lem  25157  dvferm2lem  25159  dvferm  25161  dvlip  25166  dvlipcn  25167  dvle  25180  dvivthlem1  25181  dvivth  25183  lhop1lem  25186  lhop1  25187  lhop2  25188  lhop  25189  dvfsumle  25194  dvfsumge  25195  dvfsumlem1  25199  dvfsumlem2  25200  dvfsumlem3  25201  dvfsumlem4  25202  dvfsumrlimge0  25203  dvfsumrlim  25204  dvfsumrlim2  25205  dvfsum2  25207  ftc1a  25210  ftc1cn  25216  ftc2  25217  itgsubstlem  25221  itgsubst  25222  itgpowd  25223  efcvx  25617  pige3ALT  25685  tanord  25703  divlogrlim  25799  logccv  25827  atantan  26082  amgmlem  26148  vmalogdivsum2  26695  2vmadivsumlem  26697  chpdifbndlem1  26710  selberg3lem1  26714  selberg4lem1  26717  selberg4  26718  selberg3r  26726  selberg4r  26727  selberg34r  26728  pntrlog2bndlem2  26735  pntrlog2bndlem3  26736  pntrlog2bndlem4  26737  pntrlog2bndlem5  26738  pntrlog2bndlem6  26740  pntrlog2bnd  26741  pntpbnd1a  26742  pntpbnd1  26743  pntpbnd2  26744  pntibndlem2a  26747  pntibndlem2  26748  pntibndlem3  26749  pntlemd  26751  pnt  26771  padicabv  26787  cnre2csqima  31870  ftc2re  32587  fdvposlt  32588  fdvposle  32590  itgexpif  32595  circlemeth  32629  circlemethnat  32630  circlevma  32631  circlemethhgt  32632  ioosconn  33218  iccllysconn  33221  itg2gt0cn  35841  itggt0cn  35856  ftc1cnnclem  35857  ftc1cnnc  35858  ftc1anclem8  35866  ftc2nc  35868  dvreasin  35872  dvreacos  35873  areacirclem1  35874  areacirc  35879  aks4d1p1p6  40088  aks4d1p1p5  40090  ioontr  43056  iooshift  43067  ioonct  43082  iooiinicc  43087  icomnfinre  43097  iooiinioc  43101  islptre  43167  lptioo2  43179  lptioo1  43180  limcresiooub  43190  limcresioolb  43191  limcleqr  43192  lptioo2cn  43193  lptioo1cn  43194  limclner  43199  limclr  43203  icccncfext  43435  cncfiooicclem1  43441  dvresioo  43469  dvbdfbdioolem1  43476  dvbdfbdioolem2  43477  ioodvbdlimc1lem1  43479  ioodvbdlimc1lem2  43480  ioodvbdlimc2lem  43482  itgsin0pilem1  43498  itgcoscmulx  43517  itgiccshift  43528  itgperiod  43529  itgsbtaddcnst  43530  dirkercncflem2  43652  dirkercncflem3  43653  dirkercncflem4  43654  fourierdlem16  43671  fourierdlem21  43676  fourierdlem22  43677  fourierdlem28  43683  fourierdlem48  43702  fourierdlem49  43703  fourierdlem50  43704  fourierdlem56  43710  fourierdlem57  43711  fourierdlem59  43713  fourierdlem60  43714  fourierdlem61  43715  fourierdlem65  43719  fourierdlem72  43726  fourierdlem74  43728  fourierdlem75  43729  fourierdlem76  43730  fourierdlem80  43734  fourierdlem81  43735  fourierdlem83  43737  fourierdlem84  43738  fourierdlem85  43739  fourierdlem88  43742  fourierdlem89  43743  fourierdlem90  43744  fourierdlem91  43745  fourierdlem92  43746  fourierdlem94  43748  fourierdlem95  43749  fourierdlem97  43751  fourierdlem101  43755  fourierdlem103  43757  fourierdlem104  43758  fourierdlem111  43765  fourierdlem112  43766  fourierdlem113  43767  fouriersw  43779  fouriercn  43780  ioorrnopnlem  43852  hspdifhsp  44161  hspmbllem2  44172  hspmbl  44174  iunhoiioolem  44220  smfresal  44333  smfpimbor1lem1  44343