Theorem ioossre 11638

Description: An open interval is a set of reals. (Contributed by NM, 31-May-2007.)

Assertion

Ref	Expression
ioossre	|- ( A (,) B ) C_ RR

Proof of Theorem ioossre

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		elioore 11611	. 2 |- ( x e. ( A (,) B ) -> x e. RR )
2	1	ssriv 3445	1 |- ( A (,) B ) C_ RR

Syntax hints:   C_ wss 3413  (class class class)co 6277   RRcr 9520   (,)cioo 11581

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-8 1844  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-sep 4516  ax-nul 4524  ax-pow 4571  ax-pr 4629  ax-un 6573  ax-cnex 9577  ax-resscn 9578  ax-pre-lttri 9595  ax-pre-lttrn 9596

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 975  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-eu 2242  df-mo 2243  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-nel 2601  df-ral 2758  df-rex 2759  df-rab 2762  df-v 3060  df-sbc 3277  df-csb 3373  df-dif 3416  df-un 3418  df-in 3420  df-ss 3427  df-nul 3738  df-if 3885  df-pw 3956  df-sn 3972  df-pr 3974  df-op 3978  df-uni 4191  df-iun 4272  df-br 4395  df-opab 4453  df-mpt 4454  df-id 4737  df-po 4743  df-so 4744  df-xp 4828  df-rel 4829  df-cnv 4830  df-co 4831  df-dm 4832  df-rn 4833  df-res 4834  df-ima 4835  df-iota 5532  df-fun 5570  df-fn 5571  df-f 5572  df-f1 5573  df-fo 5574  df-f1o 5575  df-fv 5576  df-ov 6280  df-oprab 6281  df-mpt2 6282  df-1st 6783  df-2nd 6784  df-er 7347  df-en 7554  df-dom 7555  df-sdom 7556  df-pnf 9659  df-mnf 9660  df-xr 9661  df-ltxr 9662  df-le 9663  df-ioo 11585

This theorem is referenced by:  ioof  11674  difreicc  11704  icopnfcld  21565  ioombl1  22262  ioorcl2  22271  uniioombllem2  22282  uniioombllem3a  22283  uniioombllem3  22284  uniioombllem4  22285  uniioombllem6  22287  ismbf3d  22351  itgsplitioo  22534  ditgeq3  22544  dvferm1lem  22675  dvferm2lem  22677  dvferm  22679  dvlip  22684  dvlipcn  22685  dvle  22698  dvivthlem1  22699  dvivth  22701  lhop1lem  22704  lhop1  22705  lhop2  22706  lhop  22707  dvfsumle  22712  dvfsumge  22713  dvfsumlem1  22717  dvfsumlem2  22718  dvfsumlem3  22719  dvfsumlem4  22720  dvfsumrlimge0  22721  dvfsumrlim  22722  dvfsumrlim2  22723  dvfsum2  22725  ftc1a  22728  ftc1cn  22734  ftc2  22735  itgsubstlem  22739  itgsubst  22740  efcvx  23134  pige3  23200  tanord  23215  divlogrlim  23308  logccv  23336  atantan  23577  amgmlem  23643  vmalogdivsum2  24102  2vmadivsumlem  24104  chpdifbndlem1  24117  selberg3lem1  24121  selberg4lem1  24124  selberg4  24125  selberg3r  24133  selberg4r  24134  selberg34r  24135  pntrlog2bndlem2  24142  pntrlog2bndlem3  24143  pntrlog2bndlem4  24144  pntrlog2bndlem5  24145  pntrlog2bndlem6  24147  pntrlog2bnd  24148  pntpbnd1a  24149  pntpbnd1  24150  pntpbnd2  24151  pntibndlem2a  24154  pntibndlem2  24155  pntibndlem3  24156  pntlemd  24158  pnt  24178  padicabv  24194  cnre2csqima  28332  iooscon  29531  iccllyscon  29534  itg2gt0cn  31423  itggt0cn  31440  ftc1cnnclem  31441  ftc1cnnc  31442  ftc1anclem8  31450  ftc2nc  31452  dvreasin  31456  dvreacos  31457  areacirclem1  31458  areacirc  31463  itgpowd  35526  ioosscn  36876  ioontr  36898  iooshift  36911  islptre  36974  lptioo2  36986  lptioo1  36987  limcresiooub  36997  limcresioolb  36998  limcleqr  36999  lptioo2cn  37000  lptioo1cn  37001  limclner  37006  limclr  37010  icccncfext  37039  cncfiooicclem1  37045  dvmptresicc  37065  dvresioo  37067  dvbdfbdioolem1  37074  dvbdfbdioolem2  37075  ioodvbdlimc1lem1  37077  ioodvbdlimc1lem2  37078  ioodvbdlimc2lem  37080  itgsin0pilem1  37097  itgcoscmulx  37117  itgiccshift  37128  itgperiod  37129  itgsbtaddcnst  37130  dirkercncflem2  37235  dirkercncflem3  37236  dirkercncflem4  37237  fourierdlem16  37254  fourierdlem21  37259  fourierdlem22  37260  fourierdlem28  37266  fourierdlem48  37286  fourierdlem49  37287  fourierdlem50  37288  fourierdlem56  37294  fourierdlem57  37295  fourierdlem59  37297  fourierdlem60  37298  fourierdlem61  37299  fourierdlem65  37303  fourierdlem72  37310  fourierdlem74  37312  fourierdlem75  37313  fourierdlem76  37314  fourierdlem80  37318  fourierdlem81  37319  fourierdlem83  37321  fourierdlem84  37322  fourierdlem85  37323  fourierdlem88  37326  fourierdlem89  37327  fourierdlem90  37328  fourierdlem91  37329  fourierdlem92  37330  fourierdlem94  37332  fourierdlem95  37333  fourierdlem97  37335  fourierdlem101  37339  fourierdlem103  37341  fourierdlem104  37342  fourierdlem111  37349  fourierdlem112  37350  fourierdlem113  37351  fouriersw  37363  fouriercn  37364