Theorem ioossre 13358

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 13326	. 2 ⊢ (𝑥 ∈ (𝐴(,)𝐵) → 𝑥 ∈ ℝ)
2	1	ssriv 3926	1 ⊢ (𝐴(,)𝐵) ⊆ ℝ

Syntax hints:   ⊆ wss 3890  (class class class)co 7363  ℝcr 11035  (,)cioo 13296

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-sep 5225  ax-nul 5235  ax-pow 5301  ax-pr 5369  ax-un 7685  ax-cnex 11092  ax-resscn 11093  ax-pre-lttri 11110  ax-pre-lttrn 11111

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ne 2936  df-nel 3040  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-sbc 3731  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-pw 4538  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-iun 4930  df-br 5080  df-opab 5142  df-mpt 5161  df-id 5520  df-po 5533  df-so 5534  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-ov 7366  df-oprab 7367  df-mpo 7368  df-1st 7938  df-2nd 7939  df-er 8640  df-en 8891  df-dom 8892  df-sdom 8893  df-pnf 11179  df-mnf 11180  df-xr 11181  df-ltxr 11182  df-le 11183  df-ioo 13300

This theorem is referenced by:  ioosscn  13359  ioof  13398  difreicc  13435  icopnfcld  24757  ioombl1  25554  ioorcl2  25564  uniioombllem2  25575  uniioombllem3a  25576  uniioombllem3  25577  uniioombllem4  25578  uniioombllem6  25580  ismbf3d  25646  itgsplitioo  25830  ditgeq3  25842  dvmptresicc  25908  dvferm1lem  25976  dvferm2lem  25978  dvferm  25980  dvlip  25985  dvlipcn  25986  dvle  25999  dvivthlem1  26000  dvivth  26002  lhop1lem  26005  lhop1  26006  lhop2  26007  lhop  26008  dvfsumle  26013  dvfsumge  26014  dvfsumlem1  26018  dvfsumlem2  26019  dvfsumlem3  26020  dvfsumlem4  26021  dvfsumrlimge0  26022  dvfsumrlim  26023  dvfsumrlim2  26024  dvfsum2  26026  ftc1a  26029  ftc1cn  26035  ftc2  26036  itgsubstlem  26040  itgsubst  26041  itgpowd  26042  efcvx  26439  pige3ALT  26509  tanord  26527  divlogrlim  26624  logccv  26652  atantan  26912  amgmlem  26978  vmalogdivsum2  27526  2vmadivsumlem  27528  chpdifbndlem1  27541  selberg3lem1  27545  selberg4lem1  27548  selberg4  27549  selberg3r  27557  selberg4r  27558  selberg34r  27559  pntrlog2bndlem2  27566  pntrlog2bndlem3  27567  pntrlog2bndlem4  27568  pntrlog2bndlem5  27569  pntrlog2bndlem6  27571  pntrlog2bnd  27572  pntpbnd1a  27573  pntpbnd1  27574  pntpbnd2  27575  pntibndlem2a  27578  pntibndlem2  27579  pntibndlem3  27580  pntlemd  27582  pnt  27602  padicabv  27618  cnre2csqima  34102  ftc2re  34789  fdvposlt  34790  fdvposle  34792  itgexpif  34797  circlemeth  34831  circlemethnat  34832  circlevma  34833  circlemethhgt  34834  ioosconn  35482  iccllysconn  35485  itg2gt0cn  38049  itggt0cn  38064  ftc1cnnclem  38065  ftc1cnnc  38066  ftc1anclem8  38074  ftc2nc  38076  dvreasin  38080  dvreacos  38081  areacirclem1  38082  areacirc  38087  aks4d1p1p6  42565  aks4d1p1p5  42567  ioontr  45963  iooshift  45974  ioonct  45989  iooiinicc  45994  icomnfinre  46004  iooiinioc  46008  islptre  46071  lptioo2  46083  lptioo1  46084  limcresiooub  46092  limcresioolb  46093  limcleqr  46094  lptioo2cn  46095  lptioo1cn  46096  limclner  46101  limclr  46105  icccncfext  46337  cncfiooicclem1  46343  dvresioo  46371  dvbdfbdioolem1  46378  dvbdfbdioolem2  46379  ioodvbdlimc1lem1  46381  ioodvbdlimc1lem2  46382  ioodvbdlimc2lem  46384  itgsin0pilem1  46400  itgcoscmulx  46419  itgiccshift  46430  itgperiod  46431  itgsbtaddcnst  46432  dirkercncflem2  46554  dirkercncflem3  46555  dirkercncflem4  46556  fourierdlem16  46573  fourierdlem21  46578  fourierdlem22  46579  fourierdlem28  46585  fourierdlem48  46604  fourierdlem49  46605  fourierdlem50  46606  fourierdlem56  46612  fourierdlem57  46613  fourierdlem59  46615  fourierdlem60  46616  fourierdlem61  46617  fourierdlem65  46621  fourierdlem72  46628  fourierdlem74  46630  fourierdlem75  46631  fourierdlem76  46632  fourierdlem80  46636  fourierdlem81  46637  fourierdlem83  46639  fourierdlem84  46640  fourierdlem85  46641  fourierdlem88  46644  fourierdlem89  46645  fourierdlem90  46646  fourierdlem91  46647  fourierdlem92  46648  fourierdlem94  46650  fourierdlem95  46651  fourierdlem97  46653  fourierdlem101  46657  fourierdlem103  46659  fourierdlem104  46660  fourierdlem111  46667  fourierdlem112  46668  fourierdlem113  46669  fouriersw  46681  fouriercn  46682  ioorrnopnlem  46754  hspdifhsp  47066  hspmbllem2  47077  hspmbl  47079  iunhoiioolem  47125  smfresal  47238  smfpimbor1lem1  47248