Theorem ioossre 12524

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

Syntax hints:   ⊆ wss 3799  (class class class)co 6906  ℝcr 10252  (,)cioo 12464

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-8 2168  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2391  ax-ext 2804  ax-sep 5006  ax-nul 5014  ax-pow 5066  ax-pr 5128  ax-un 7210  ax-cnex 10309  ax-resscn 10310  ax-pre-lttri 10327  ax-pre-lttrn 10328

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-3or 1114  df-3an 1115  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-mo 2606  df-eu 2641  df-clab 2813  df-cleq 2819  df-clel 2822  df-nfc 2959  df-ne 3001  df-nel 3104  df-ral 3123  df-rex 3124  df-rab 3127  df-v 3417  df-sbc 3664  df-csb 3759  df-dif 3802  df-un 3804  df-in 3806  df-ss 3813  df-nul 4146  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-op 4405  df-uni 4660  df-iun 4743  df-br 4875  df-opab 4937  df-mpt 4954  df-id 5251  df-po 5264  df-so 5265  df-xp 5349  df-rel 5350  df-cnv 5351  df-co 5352  df-dm 5353  df-rn 5354  df-res 5355  df-ima 5356  df-iota 6087  df-fun 6126  df-fn 6127  df-f 6128  df-f1 6129  df-fo 6130  df-f1o 6131  df-fv 6132  df-ov 6909  df-oprab 6910  df-mpt2 6911  df-1st 7429  df-2nd 7430  df-er 8010  df-en 8224  df-dom 8225  df-sdom 8226  df-pnf 10394  df-mnf 10395  df-xr 10396  df-ltxr 10397  df-le 10398  df-ioo 12468

This theorem is referenced by:  ioof  12561  difreicc  12598  icopnfcld  22942  ioombl1  23729  ioorcl2  23739  uniioombllem2  23750  uniioombllem3a  23751  uniioombllem3  23752  uniioombllem4  23753  uniioombllem6  23755  ismbf3d  23821  itgsplitioo  24004  ditgeq3  24014  dvferm1lem  24147  dvferm2lem  24149  dvferm  24151  dvlip  24156  dvlipcn  24157  dvle  24170  dvivthlem1  24171  dvivth  24173  lhop1lem  24176  lhop1  24177  lhop2  24178  lhop  24179  dvfsumle  24184  dvfsumge  24185  dvfsumlem1  24189  dvfsumlem2  24190  dvfsumlem3  24191  dvfsumlem4  24192  dvfsumrlimge0  24193  dvfsumrlim  24194  dvfsumrlim2  24195  dvfsum2  24197  ftc1a  24200  ftc1cn  24206  ftc2  24207  itgsubstlem  24211  itgsubst  24212  efcvx  24603  pige3  24670  tanord  24685  divlogrlim  24781  logccv  24809  atantan  25064  amgmlem  25130  vmalogdivsum2  25641  2vmadivsumlem  25643  chpdifbndlem1  25656  selberg3lem1  25660  selberg4lem1  25663  selberg4  25664  selberg3r  25672  selberg4r  25673  selberg34r  25674  pntrlog2bndlem2  25681  pntrlog2bndlem3  25682  pntrlog2bndlem4  25683  pntrlog2bndlem5  25684  pntrlog2bndlem6  25686  pntrlog2bnd  25687  pntpbnd1a  25688  pntpbnd1  25689  pntpbnd2  25690  pntibndlem2a  25693  pntibndlem2  25694  pntibndlem3  25695  pntlemd  25697  pnt  25717  padicabv  25733  cnre2csqima  30503  ftc2re  31226  fdvposlt  31227  fdvposle  31229  itgexpif  31234  circlemeth  31268  circlemethnat  31269  circlevma  31270  circlemethhgt  31271  ioosconn  31776  iccllysconn  31779  itg2gt0cn  34009  itggt0cn  34026  ftc1cnnclem  34027  ftc1cnnc  34028  ftc1anclem8  34036  ftc2nc  34038  dvreasin  34042  dvreacos  34043  areacirclem1  34044  areacirc  34049  itgpowd  38643  ioosscn  40516  ioontr  40534  iooshift  40545  ioonct  40560  iooiinicc  40565  icomnfinre  40575  iooiinioc  40579  islptre  40647  lptioo2  40659  lptioo1  40660  limcresiooub  40670  limcresioolb  40671  limcleqr  40672  lptioo2cn  40673  lptioo1cn  40674  limclner  40679  limclr  40683  icccncfext  40896  cncfiooicclem1  40902  dvmptresicc  40930  dvresioo  40932  dvbdfbdioolem1  40939  dvbdfbdioolem2  40940  ioodvbdlimc1lem1  40942  ioodvbdlimc1lem2  40943  ioodvbdlimc2lem  40945  itgsin0pilem1  40961  itgcoscmulx  40980  itgiccshift  40991  itgperiod  40992  itgsbtaddcnst  40993  dirkercncflem2  41116  dirkercncflem3  41117  dirkercncflem4  41118  fourierdlem16  41135  fourierdlem21  41140  fourierdlem22  41141  fourierdlem28  41147  fourierdlem48  41166  fourierdlem49  41167  fourierdlem50  41168  fourierdlem56  41174  fourierdlem57  41175  fourierdlem59  41177  fourierdlem60  41178  fourierdlem61  41179  fourierdlem65  41183  fourierdlem72  41190  fourierdlem74  41192  fourierdlem75  41193  fourierdlem76  41194  fourierdlem80  41198  fourierdlem81  41199  fourierdlem83  41201  fourierdlem84  41202  fourierdlem85  41203  fourierdlem88  41206  fourierdlem89  41207  fourierdlem90  41208  fourierdlem91  41209  fourierdlem92  41210  fourierdlem94  41212  fourierdlem95  41213  fourierdlem97  41215  fourierdlem101  41219  fourierdlem103  41221  fourierdlem104  41222  fourierdlem111  41229  fourierdlem112  41230  fourierdlem113  41231  fouriersw  41243  fouriercn  41244  ioorrnopnlem  41316  hspdifhsp  41625  hspmbllem2  41636  hspmbl  41638  iunhoiioolem  41684  smfresal  41790  smfpimbor1lem1  41800