Theorem ioossre 13519

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

This proof depends on syntax axioms:   ⊆ wss 3899  (class class class)co 7412  ℝcr 11180  (,)cioo 13457

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7740  ax-cnex 11237  ax-resscn 11238  ax-pre-lttri 11255  ax-pre-lttrn 11256

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3063  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5546  df-po 5559  df-so 5560  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6487  df-fun 6533  df-fn 6534  df-f 6535  df-f1 6536  df-fo 6537  df-f1o 6538  df-fv 6539  df-ov 7415  df-oprab 7416  df-mpo 7417  df-1st 7990  df-2nd 7991  df-er 8701  df-en 8958  df-dom 8959  df-sdom 8960  df-pnf 11326  df-mnf 11327  df-xr 11328  df-ltxr 11329  df-le 11330  df-ioo 13461

This theorem is used by:  ioosscn  13520  ioof  13559  difreicc  13596  icopnfcld  25066  ioombl1  25863  ioorcl2  25873  uniioombllem2  25884  uniioombllem3a  25885  uniioombllem3  25886  uniioombllem4  25887  uniioombllem6  25889  ismbf3d  25955  itgsplitioo  26138  ditgeq3  26150  dvmptresicc  26216  dvferm1lem  26284  dvferm2lem  26286  dvferm  26288  dvlip  26293  dvlipcn  26294  dvle  26307  dvivthlem1  26308  dvivth  26310  lhop1lem  26313  lhop1  26314  lhop2  26315  lhop  26316  dvfsumle  26321  dvfsumge  26322  dvfsumlem1  26326  dvfsumlem2  26327  dvfsumlem3  26328  dvfsumlem4  26329  dvfsumrlimge0  26330  dvfsumrlim  26331  dvfsumrlim2  26332  dvfsum2  26334  ftc1a  26337  ftc1cn  26343  ftc2  26344  itgsubstlem  26348  itgsubst  26349  itgpowd  26350  efcvx  26758  pige3ALT  26830  tanord  26848  divlogrlim  26945  logccv  26973  atantan  27233  amgmlem  27299  vmalogdivsum2  27847  2vmadivsumlem  27849  chpdifbndlem1  27862  selberg3lem1  27866  selberg4lem1  27869  selberg4  27870  selberg3r  27878  selberg4r  27879  selberg34r  27880  pntrlog2bndlem2  27887  pntrlog2bndlem3  27888  pntrlog2bndlem4  27889  pntrlog2bndlem5  27890  pntrlog2bndlem6  27892  pntrlog2bnd  27893  pntpbnd1a  27894  pntpbnd1  27895  pntpbnd2  27896  pntibndlem2a  27899  pntibndlem2  27900  pntibndlem3  27901  pntlemd  27903  pnt  27923  padicabv  27939  cnre2csqima  34525  ftc2re  35210  fdvposlt  35211  fdvposle  35213  itgexpif  35218  circlemeth  35252  circlemethnat  35253  circlevma  35254  circlemethhgt  35255  ioosconn  35981  iccllysconn  35984  itg2gt0cn  38561  itggt0cn  38576  ftc1cnnclem  38577  ftc1cnnc  38578  ftc1anclem8  38586  ftc2nc  38588  dvreasin  38592  dvreacos  38593  areacirclem1  38594  areacirc  38599  aks4d1p1p6  43091  aks4d1p1p5  43093  ioontr  46467  iooshift  46478  ioonct  46493  iooiinicc  46498  icomnfinre  46508  iooiinioc  46512  islptre  46575  lptioo2  46587  lptioo1  46588  limcresiooub  46596  limcresioolb  46597  limcleqr  46598  lptioo2cn  46599  lptioo1cn  46600  limclner  46605  limclr  46609  icccncfext  46841  cncfiooicclem1  46847  dvresioo  46875  dvbdfbdioolem1  46882  dvbdfbdioolem2  46883  ioodvbdlimc1lem1  46885  ioodvbdlimc1lem2  46886  ioodvbdlimc2lem  46888  itgsin0pilem1  46904  itgcoscmulx  46923  itgiccshift  46934  itgperiod  46935  itgsbtaddcnst  46936  dirkercncflem2  47058  dirkercncflem3  47059  dirkercncflem4  47060  fourierdlem16  47077  fourierdlem21  47082  fourierdlem22  47083  fourierdlem28  47089  fourierdlem48  47108  fourierdlem49  47109  fourierdlem50  47110  fourierdlem56  47116  fourierdlem57  47117  fourierdlem59  47119  fourierdlem60  47120  fourierdlem61  47121  fourierdlem65  47125  fourierdlem72  47132  fourierdlem74  47134  fourierdlem75  47135  fourierdlem76  47136  fourierdlem80  47140  fourierdlem81  47141  fourierdlem83  47143  fourierdlem84  47144  fourierdlem85  47145  fourierdlem88  47148  fourierdlem89  47149  fourierdlem90  47150  fourierdlem91  47151  fourierdlem92  47152  fourierdlem94  47154  fourierdlem95  47155  fourierdlem97  47157  fourierdlem101  47161  fourierdlem103  47163  fourierdlem104  47164  fourierdlem111  47171  fourierdlem112  47172  fourierdlem113  47173  fouriersw  47185  fouriercn  47186  ioorrnopnlem  47258  hspdifhsp  47570  hspmbllem2  47581  hspmbl  47583  iunhoiioolem  47629  smfresal  47742  smfpimbor1lem1  47752