Theorem ioossre 13389

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

Syntax hints:   ⊆ wss 3948  (class class class)co 7411  ℝcr 11111  (,)cioo 13328

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7727  ax-cnex 11168  ax-resscn 11169  ax-pre-lttri 11186  ax-pre-lttrn 11187

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-po 5588  df-so 5589  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-ov 7414  df-oprab 7415  df-mpo 7416  df-1st 7977  df-2nd 7978  df-er 8705  df-en 8942  df-dom 8943  df-sdom 8944  df-pnf 11254  df-mnf 11255  df-xr 11256  df-ltxr 11257  df-le 11258  df-ioo 13332

This theorem is referenced by:  ioosscn  13390  ioof  13428  difreicc  13465  icopnfcld  24504  ioombl1  25303  ioorcl2  25313  uniioombllem2  25324  uniioombllem3a  25325  uniioombllem3  25326  uniioombllem4  25327  uniioombllem6  25329  ismbf3d  25395  itgsplitioo  25579  ditgeq3  25591  dvmptresicc  25657  dvferm1lem  25725  dvferm2lem  25727  dvferm  25729  dvlip  25734  dvlipcn  25735  dvle  25748  dvivthlem1  25749  dvivth  25751  lhop1lem  25754  lhop1  25755  lhop2  25756  lhop  25757  dvfsumle  25762  dvfsumge  25763  dvfsumlem1  25767  dvfsumlem2  25768  dvfsumlem3  25769  dvfsumlem4  25770  dvfsumrlimge0  25771  dvfsumrlim  25772  dvfsumrlim2  25773  dvfsum2  25775  ftc1a  25778  ftc1cn  25784  ftc2  25785  itgsubstlem  25789  itgsubst  25790  itgpowd  25791  efcvx  26185  pige3ALT  26253  tanord  26271  divlogrlim  26367  logccv  26395  atantan  26652  amgmlem  26718  vmalogdivsum2  27265  2vmadivsumlem  27267  chpdifbndlem1  27280  selberg3lem1  27284  selberg4lem1  27287  selberg4  27288  selberg3r  27296  selberg4r  27297  selberg34r  27298  pntrlog2bndlem2  27305  pntrlog2bndlem3  27306  pntrlog2bndlem4  27307  pntrlog2bndlem5  27308  pntrlog2bndlem6  27310  pntrlog2bnd  27311  pntpbnd1a  27312  pntpbnd1  27313  pntpbnd2  27314  pntibndlem2a  27317  pntibndlem2  27318  pntibndlem3  27319  pntlemd  27321  pnt  27341  padicabv  27357  cnre2csqima  33177  ftc2re  33896  fdvposlt  33897  fdvposle  33899  itgexpif  33904  circlemeth  33938  circlemethnat  33939  circlevma  33940  circlemethhgt  33941  ioosconn  34524  iccllysconn  34527  gg-dvfsumle  35468  gg-dvfsumlem2  35469  itg2gt0cn  36846  itggt0cn  36861  ftc1cnnclem  36862  ftc1cnnc  36863  ftc1anclem8  36871  ftc2nc  36873  dvreasin  36877  dvreacos  36878  areacirclem1  36879  areacirc  36884  aks4d1p1p6  41244  aks4d1p1p5  41246  ioontr  44523  iooshift  44534  ioonct  44549  iooiinicc  44554  icomnfinre  44564  iooiinioc  44568  islptre  44634  lptioo2  44646  lptioo1  44647  limcresiooub  44657  limcresioolb  44658  limcleqr  44659  lptioo2cn  44660  lptioo1cn  44661  limclner  44666  limclr  44670  icccncfext  44902  cncfiooicclem1  44908  dvresioo  44936  dvbdfbdioolem1  44943  dvbdfbdioolem2  44944  ioodvbdlimc1lem1  44946  ioodvbdlimc1lem2  44947  ioodvbdlimc2lem  44949  itgsin0pilem1  44965  itgcoscmulx  44984  itgiccshift  44995  itgperiod  44996  itgsbtaddcnst  44997  dirkercncflem2  45119  dirkercncflem3  45120  dirkercncflem4  45121  fourierdlem16  45138  fourierdlem21  45143  fourierdlem22  45144  fourierdlem28  45150  fourierdlem48  45169  fourierdlem49  45170  fourierdlem50  45171  fourierdlem56  45177  fourierdlem57  45178  fourierdlem59  45180  fourierdlem60  45181  fourierdlem61  45182  fourierdlem65  45186  fourierdlem72  45193  fourierdlem74  45195  fourierdlem75  45196  fourierdlem76  45197  fourierdlem80  45201  fourierdlem81  45202  fourierdlem83  45204  fourierdlem84  45205  fourierdlem85  45206  fourierdlem88  45209  fourierdlem89  45210  fourierdlem90  45211  fourierdlem91  45212  fourierdlem92  45213  fourierdlem94  45215  fourierdlem95  45216  fourierdlem97  45218  fourierdlem101  45222  fourierdlem103  45224  fourierdlem104  45225  fourierdlem111  45232  fourierdlem112  45233  fourierdlem113  45234  fouriersw  45246  fouriercn  45247  ioorrnopnlem  45319  hspdifhsp  45631  hspmbllem2  45642  hspmbl  45644  iunhoiioolem  45690  smfresal  45803  smfpimbor1lem1  45813