Theorem ioossre 12799

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

Syntax hints:   ⊆ wss 3936  (class class class)co 7156  ℝcr 10536  (,)cioo 12739

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pow 5266  ax-pr 5330  ax-un 7461  ax-cnex 10593  ax-resscn 10594  ax-pre-lttri 10611  ax-pre-lttrn 10612

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-iun 4921  df-br 5067  df-opab 5129  df-mpt 5147  df-id 5460  df-po 5474  df-so 5475  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568  df-iota 6314  df-fun 6357  df-fn 6358  df-f 6359  df-f1 6360  df-fo 6361  df-f1o 6362  df-fv 6363  df-ov 7159  df-oprab 7160  df-mpo 7161  df-1st 7689  df-2nd 7690  df-er 8289  df-en 8510  df-dom 8511  df-sdom 8512  df-pnf 10677  df-mnf 10678  df-xr 10679  df-ltxr 10680  df-le 10681  df-ioo 12743

This theorem is referenced by:  ioof  12836  difreicc  12871  icopnfcld  23376  ioombl1  24163  ioorcl2  24173  uniioombllem2  24184  uniioombllem3a  24185  uniioombllem3  24186  uniioombllem4  24187  uniioombllem6  24189  ismbf3d  24255  itgsplitioo  24438  ditgeq3  24448  dvferm1lem  24581  dvferm2lem  24583  dvferm  24585  dvlip  24590  dvlipcn  24591  dvle  24604  dvivthlem1  24605  dvivth  24607  lhop1lem  24610  lhop1  24611  lhop2  24612  lhop  24613  dvfsumle  24618  dvfsumge  24619  dvfsumlem1  24623  dvfsumlem2  24624  dvfsumlem3  24625  dvfsumlem4  24626  dvfsumrlimge0  24627  dvfsumrlim  24628  dvfsumrlim2  24629  dvfsum2  24631  ftc1a  24634  ftc1cn  24640  ftc2  24641  itgsubstlem  24645  itgsubst  24646  efcvx  25037  pige3ALT  25105  tanord  25122  divlogrlim  25218  logccv  25246  atantan  25501  amgmlem  25567  vmalogdivsum2  26114  2vmadivsumlem  26116  chpdifbndlem1  26129  selberg3lem1  26133  selberg4lem1  26136  selberg4  26137  selberg3r  26145  selberg4r  26146  selberg34r  26147  pntrlog2bndlem2  26154  pntrlog2bndlem3  26155  pntrlog2bndlem4  26156  pntrlog2bndlem5  26157  pntrlog2bndlem6  26159  pntrlog2bnd  26160  pntpbnd1a  26161  pntpbnd1  26162  pntpbnd2  26163  pntibndlem2a  26166  pntibndlem2  26167  pntibndlem3  26168  pntlemd  26170  pnt  26190  padicabv  26206  cnre2csqima  31154  ftc2re  31869  fdvposlt  31870  fdvposle  31872  itgexpif  31877  circlemeth  31911  circlemethnat  31912  circlevma  31913  circlemethhgt  31914  ioosconn  32494  iccllysconn  32497  itg2gt0cn  34962  itggt0cn  34979  ftc1cnnclem  34980  ftc1cnnc  34981  ftc1anclem8  34989  ftc2nc  34991  dvreasin  34995  dvreacos  34996  areacirclem1  34997  areacirc  35002  itgpowd  39841  ioosscn  41789  ioontr  41807  iooshift  41818  ioonct  41833  iooiinicc  41838  icomnfinre  41848  iooiinioc  41852  islptre  41920  lptioo2  41932  lptioo1  41933  limcresiooub  41943  limcresioolb  41944  limcleqr  41945  lptioo2cn  41946  lptioo1cn  41947  limclner  41952  limclr  41956  icccncfext  42190  cncfiooicclem1  42196  dvmptresicc  42224  dvresioo  42226  dvbdfbdioolem1  42233  dvbdfbdioolem2  42234  ioodvbdlimc1lem1  42236  ioodvbdlimc1lem2  42237  ioodvbdlimc2lem  42239  itgsin0pilem1  42255  itgcoscmulx  42274  itgiccshift  42285  itgperiod  42286  itgsbtaddcnst  42287  dirkercncflem2  42409  dirkercncflem3  42410  dirkercncflem4  42411  fourierdlem16  42428  fourierdlem21  42433  fourierdlem22  42434  fourierdlem28  42440  fourierdlem48  42459  fourierdlem49  42460  fourierdlem50  42461  fourierdlem56  42467  fourierdlem57  42468  fourierdlem59  42470  fourierdlem60  42471  fourierdlem61  42472  fourierdlem65  42476  fourierdlem72  42483  fourierdlem74  42485  fourierdlem75  42486  fourierdlem76  42487  fourierdlem80  42491  fourierdlem81  42492  fourierdlem83  42494  fourierdlem84  42495  fourierdlem85  42496  fourierdlem88  42499  fourierdlem89  42500  fourierdlem90  42501  fourierdlem91  42502  fourierdlem92  42503  fourierdlem94  42505  fourierdlem95  42506  fourierdlem97  42508  fourierdlem101  42512  fourierdlem103  42514  fourierdlem104  42515  fourierdlem111  42522  fourierdlem112  42523  fourierdlem113  42524  fouriersw  42536  fouriercn  42537  ioorrnopnlem  42609  hspdifhsp  42918  hspmbllem2  42929  hspmbl  42931  iunhoiioolem  42977  smfresal  43083  smfpimbor1lem1  43093