Theorem ioossre 13311

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

Syntax hints:   ⊆ wss 3898  (class class class)co 7354  ℝcr 11014  (,)cioo 13249

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7676  ax-cnex 11071  ax-resscn 11072  ax-pre-lttri 11089  ax-pre-lttrn 11090

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ne 2930  df-nel 3034  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-sbc 3738  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-iun 4945  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5516  df-po 5529  df-so 5530  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-iota 6444  df-fun 6490  df-fn 6491  df-f 6492  df-f1 6493  df-fo 6494  df-f1o 6495  df-fv 6496  df-ov 7357  df-oprab 7358  df-mpo 7359  df-1st 7929  df-2nd 7930  df-er 8630  df-en 8878  df-dom 8879  df-sdom 8880  df-pnf 11157  df-mnf 11158  df-xr 11159  df-ltxr 11160  df-le 11161  df-ioo 13253

This theorem is referenced by:  ioosscn  13312  ioof  13351  difreicc  13388  icopnfcld  24685  ioombl1  25493  ioorcl2  25503  uniioombllem2  25514  uniioombllem3a  25515  uniioombllem3  25516  uniioombllem4  25517  uniioombllem6  25519  ismbf3d  25585  itgsplitioo  25769  ditgeq3  25781  dvmptresicc  25847  dvferm1lem  25918  dvferm2lem  25920  dvferm  25922  dvlip  25928  dvlipcn  25929  dvle  25942  dvivthlem1  25943  dvivth  25945  lhop1lem  25948  lhop1  25949  lhop2  25950  lhop  25951  dvfsumle  25956  dvfsumleOLD  25957  dvfsumge  25958  dvfsumlem1  25962  dvfsumlem2  25963  dvfsumlem2OLD  25964  dvfsumlem3  25965  dvfsumlem4  25966  dvfsumrlimge0  25967  dvfsumrlim  25968  dvfsumrlim2  25969  dvfsum2  25971  ftc1a  25974  ftc1cn  25980  ftc2  25981  itgsubstlem  25985  itgsubst  25986  itgpowd  25987  efcvx  26389  pige3ALT  26459  tanord  26477  divlogrlim  26574  logccv  26602  atantan  26863  amgmlem  26930  vmalogdivsum2  27479  2vmadivsumlem  27481  chpdifbndlem1  27494  selberg3lem1  27498  selberg4lem1  27501  selberg4  27502  selberg3r  27510  selberg4r  27511  selberg34r  27512  pntrlog2bndlem2  27519  pntrlog2bndlem3  27520  pntrlog2bndlem4  27521  pntrlog2bndlem5  27522  pntrlog2bndlem6  27524  pntrlog2bnd  27525  pntpbnd1a  27526  pntpbnd1  27527  pntpbnd2  27528  pntibndlem2a  27531  pntibndlem2  27532  pntibndlem3  27533  pntlemd  27535  pnt  27555  padicabv  27571  cnre2csqima  33947  ftc2re  34634  fdvposlt  34635  fdvposle  34637  itgexpif  34642  circlemeth  34676  circlemethnat  34677  circlevma  34678  circlemethhgt  34679  ioosconn  35314  iccllysconn  35317  itg2gt0cn  37738  itggt0cn  37753  ftc1cnnclem  37754  ftc1cnnc  37755  ftc1anclem8  37763  ftc2nc  37765  dvreasin  37769  dvreacos  37770  areacirclem1  37771  areacirc  37776  aks4d1p1p6  42189  aks4d1p1p5  42191  ioontr  45638  iooshift  45649  ioonct  45664  iooiinicc  45669  icomnfinre  45679  iooiinioc  45683  islptre  45746  lptioo2  45758  lptioo1  45759  limcresiooub  45767  limcresioolb  45768  limcleqr  45769  lptioo2cn  45770  lptioo1cn  45771  limclner  45776  limclr  45780  icccncfext  46012  cncfiooicclem1  46018  dvresioo  46046  dvbdfbdioolem1  46053  dvbdfbdioolem2  46054  ioodvbdlimc1lem1  46056  ioodvbdlimc1lem2  46057  ioodvbdlimc2lem  46059  itgsin0pilem1  46075  itgcoscmulx  46094  itgiccshift  46105  itgperiod  46106  itgsbtaddcnst  46107  dirkercncflem2  46229  dirkercncflem3  46230  dirkercncflem4  46231  fourierdlem16  46248  fourierdlem21  46253  fourierdlem22  46254  fourierdlem28  46260  fourierdlem48  46279  fourierdlem49  46280  fourierdlem50  46281  fourierdlem56  46287  fourierdlem57  46288  fourierdlem59  46290  fourierdlem60  46291  fourierdlem61  46292  fourierdlem65  46296  fourierdlem72  46303  fourierdlem74  46305  fourierdlem75  46306  fourierdlem76  46307  fourierdlem80  46311  fourierdlem81  46312  fourierdlem83  46314  fourierdlem84  46315  fourierdlem85  46316  fourierdlem88  46319  fourierdlem89  46320  fourierdlem90  46321  fourierdlem91  46322  fourierdlem92  46323  fourierdlem94  46325  fourierdlem95  46326  fourierdlem97  46328  fourierdlem101  46332  fourierdlem103  46334  fourierdlem104  46335  fourierdlem111  46342  fourierdlem112  46343  fourierdlem113  46344  fouriersw  46356  fouriercn  46357  ioorrnopnlem  46429  hspdifhsp  46741  hspmbllem2  46752  hspmbl  46754  iunhoiioolem  46800  smfresal  46913  smfpimbor1lem1  46923