Theorem ioossre 13404

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

Syntax hints:   ⊆ wss 3902  (class class class)co 7390  ℝcr 11065  (,)cioo 13342

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5243  ax-nul 5253  ax-pow 5319  ax-pr 5387  ax-un 7712  ax-cnex 11122  ax-resscn 11123  ax-pre-lttri 11140  ax-pre-lttrn 11141

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1098  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3061  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-iun 4948  df-br 5098  df-opab 5160  df-mpt 5179  df-id 5538  df-po 5551  df-so 5552  df-xp 5649  df-rel 5650  df-cnv 5651  df-co 5652  df-dm 5653  df-rn 5654  df-res 5655  df-ima 5656  df-iota 6471  df-fun 6517  df-fn 6518  df-f 6519  df-f1 6520  df-fo 6521  df-f1o 6522  df-fv 6523  df-ov 7393  df-oprab 7394  df-mpo 7395  df-1st 7964  df-2nd 7965  df-er 8671  df-en 8921  df-dom 8922  df-sdom 8923  df-pnf 11211  df-mnf 11212  df-xr 11213  df-ltxr 11214  df-le 11215  df-ioo 13346

This theorem is referenced by:  ioosscn  13405  ioof  13444  difreicc  13481  icopnfcld  24814  ioombl1  25611  ioorcl2  25621  uniioombllem2  25632  uniioombllem3a  25633  uniioombllem3  25634  uniioombllem4  25635  uniioombllem6  25637  ismbf3d  25703  itgsplitioo  25887  ditgeq3  25899  dvmptresicc  25965  dvferm1lem  26033  dvferm2lem  26035  dvferm  26037  dvlip  26042  dvlipcn  26043  dvle  26056  dvivthlem1  26057  dvivth  26059  lhop1lem  26062  lhop1  26063  lhop2  26064  lhop  26065  dvfsumle  26070  dvfsumge  26071  dvfsumlem1  26075  dvfsumlem2  26076  dvfsumlem3  26077  dvfsumlem4  26078  dvfsumrlimge0  26079  dvfsumrlim  26080  dvfsumrlim2  26081  dvfsum2  26083  ftc1a  26086  ftc1cn  26092  ftc2  26093  itgsubstlem  26097  itgsubst  26098  itgpowd  26099  efcvx  26499  pige3ALT  26572  tanord  26590  divlogrlim  26687  logccv  26715  atantan  26975  amgmlem  27041  vmalogdivsum2  27589  2vmadivsumlem  27591  chpdifbndlem1  27604  selberg3lem1  27608  selberg4lem1  27611  selberg4  27612  selberg3r  27620  selberg4r  27621  selberg34r  27622  pntrlog2bndlem2  27629  pntrlog2bndlem3  27630  pntrlog2bndlem4  27631  pntrlog2bndlem5  27632  pntrlog2bndlem6  27634  pntrlog2bnd  27635  pntpbnd1a  27636  pntpbnd1  27637  pntpbnd2  27638  pntibndlem2a  27641  pntibndlem2  27642  pntibndlem3  27643  pntlemd  27645  pnt  27665  padicabv  27681  cnre2csqima  34168  ftc2re  34852  fdvposlt  34853  fdvposle  34855  itgexpif  34860  circlemeth  34894  circlemethnat  34895  circlevma  34896  circlemethhgt  34897  ioosconn  35557  iccllysconn  35560  itg2gt0cn  38134  itggt0cn  38149  ftc1cnnclem  38150  ftc1cnnc  38151  ftc1anclem8  38159  ftc2nc  38161  dvreasin  38165  dvreacos  38166  areacirclem1  38167  areacirc  38172  aks4d1p1p6  42650  aks4d1p1p5  42652  ioontr  46047  iooshift  46058  ioonct  46073  iooiinicc  46078  icomnfinre  46088  iooiinioc  46092  islptre  46155  lptioo2  46167  lptioo1  46168  limcresiooub  46176  limcresioolb  46177  limcleqr  46178  lptioo2cn  46179  lptioo1cn  46180  limclner  46185  limclr  46189  icccncfext  46421  cncfiooicclem1  46427  dvresioo  46455  dvbdfbdioolem1  46462  dvbdfbdioolem2  46463  ioodvbdlimc1lem1  46465  ioodvbdlimc1lem2  46466  ioodvbdlimc2lem  46468  itgsin0pilem1  46484  itgcoscmulx  46503  itgiccshift  46514  itgperiod  46515  itgsbtaddcnst  46516  dirkercncflem2  46638  dirkercncflem3  46639  dirkercncflem4  46640  fourierdlem16  46657  fourierdlem21  46662  fourierdlem22  46663  fourierdlem28  46669  fourierdlem48  46688  fourierdlem49  46689  fourierdlem50  46690  fourierdlem56  46696  fourierdlem57  46697  fourierdlem59  46699  fourierdlem60  46700  fourierdlem61  46701  fourierdlem65  46705  fourierdlem72  46712  fourierdlem74  46714  fourierdlem75  46715  fourierdlem76  46716  fourierdlem80  46720  fourierdlem81  46721  fourierdlem83  46723  fourierdlem84  46724  fourierdlem85  46725  fourierdlem88  46728  fourierdlem89  46729  fourierdlem90  46730  fourierdlem91  46731  fourierdlem92  46732  fourierdlem94  46734  fourierdlem95  46735  fourierdlem97  46737  fourierdlem101  46741  fourierdlem103  46743  fourierdlem104  46744  fourierdlem111  46751  fourierdlem112  46752  fourierdlem113  46753  fouriersw  46765  fouriercn  46766  ioorrnopnlem  46838  hspdifhsp  47150  hspmbllem2  47161  hspmbl  47163  iunhoiioolem  47209  smfresal  47322  smfpimbor1lem1  47332