Theorem ioossre 13422

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

Syntax hints:   ⊆ wss 3907  (class class class)co 7400  ℝcr 11087  (,)cioo 13360

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-sep 5250  ax-nul 5260  ax-pow 5326  ax-pr 5394  ax-un 7722  ax-cnex 11144  ax-resscn 11145  ax-pre-lttri 11162  ax-pre-lttrn 11163

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-nel 3065  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-sbc 3748  df-csb 3856  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-pw 4560  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-iun 4953  df-br 5105  df-opab 5167  df-mpt 5186  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 6481  df-fun 6527  df-fn 6528  df-f 6529  df-f1 6530  df-fo 6531  df-f1o 6532  df-fv 6533  df-ov 7403  df-oprab 7404  df-mpo 7405  df-1st 7974  df-2nd 7975  df-er 8682  df-en 8932  df-dom 8933  df-sdom 8934  df-pnf 11233  df-mnf 11234  df-xr 11235  df-ltxr 11236  df-le 11237  df-ioo 13364

This theorem is referenced by:  ioosscn  13423  ioof  13462  difreicc  13499  icopnfcld  24881  ioombl1  25678  ioorcl2  25688  uniioombllem2  25699  uniioombllem3a  25700  uniioombllem3  25701  uniioombllem4  25702  uniioombllem6  25704  ismbf3d  25770  itgsplitioo  25954  ditgeq3  25966  dvmptresicc  26032  dvferm1lem  26100  dvferm2lem  26102  dvferm  26104  dvlip  26109  dvlipcn  26110  dvle  26123  dvivthlem1  26124  dvivth  26126  lhop1lem  26129  lhop1  26130  lhop2  26131  lhop  26132  dvfsumle  26137  dvfsumge  26138  dvfsumlem1  26142  dvfsumlem2  26143  dvfsumlem3  26144  dvfsumlem4  26145  dvfsumrlimge0  26146  dvfsumrlim  26147  dvfsumrlim2  26148  dvfsum2  26150  ftc1a  26153  ftc1cn  26159  ftc2  26160  itgsubstlem  26164  itgsubst  26165  itgpowd  26166  efcvx  26566  pige3ALT  26639  tanord  26657  divlogrlim  26754  logccv  26782  atantan  27042  amgmlem  27108  vmalogdivsum2  27656  2vmadivsumlem  27658  chpdifbndlem1  27671  selberg3lem1  27675  selberg4lem1  27678  selberg4  27679  selberg3r  27687  selberg4r  27688  selberg34r  27689  pntrlog2bndlem2  27696  pntrlog2bndlem3  27697  pntrlog2bndlem4  27698  pntrlog2bndlem5  27699  pntrlog2bndlem6  27701  pntrlog2bnd  27702  pntpbnd1a  27703  pntpbnd1  27704  pntpbnd2  27705  pntibndlem2a  27708  pntibndlem2  27709  pntibndlem3  27710  pntlemd  27712  pnt  27732  padicabv  27748  cnre2csqima  34213  ftc2re  34897  fdvposlt  34898  fdvposle  34900  itgexpif  34905  circlemeth  34939  circlemethnat  34940  circlevma  34941  circlemethhgt  34942  ioosconn  35605  iccllysconn  35608  itg2gt0cn  38181  itggt0cn  38196  ftc1cnnclem  38197  ftc1cnnc  38198  ftc1anclem8  38206  ftc2nc  38208  dvreasin  38212  dvreacos  38213  areacirclem1  38214  areacirc  38219  aks4d1p1p6  42697  aks4d1p1p5  42699  ioontr  46086  iooshift  46097  ioonct  46112  iooiinicc  46117  icomnfinre  46127  iooiinioc  46131  islptre  46194  lptioo2  46206  lptioo1  46207  limcresiooub  46215  limcresioolb  46216  limcleqr  46217  lptioo2cn  46218  lptioo1cn  46219  limclner  46224  limclr  46228  icccncfext  46460  cncfiooicclem1  46466  dvresioo  46494  dvbdfbdioolem1  46501  dvbdfbdioolem2  46502  ioodvbdlimc1lem1  46504  ioodvbdlimc1lem2  46505  ioodvbdlimc2lem  46507  itgsin0pilem1  46523  itgcoscmulx  46542  itgiccshift  46553  itgperiod  46554  itgsbtaddcnst  46555  dirkercncflem2  46677  dirkercncflem3  46678  dirkercncflem4  46679  fourierdlem16  46696  fourierdlem21  46701  fourierdlem22  46702  fourierdlem28  46708  fourierdlem48  46727  fourierdlem49  46728  fourierdlem50  46729  fourierdlem56  46735  fourierdlem57  46736  fourierdlem59  46738  fourierdlem60  46739  fourierdlem61  46740  fourierdlem65  46744  fourierdlem72  46751  fourierdlem74  46753  fourierdlem75  46754  fourierdlem76  46755  fourierdlem80  46759  fourierdlem81  46760  fourierdlem83  46762  fourierdlem84  46763  fourierdlem85  46764  fourierdlem88  46767  fourierdlem89  46768  fourierdlem90  46769  fourierdlem91  46770  fourierdlem92  46771  fourierdlem94  46773  fourierdlem95  46774  fourierdlem97  46776  fourierdlem101  46780  fourierdlem103  46782  fourierdlem104  46783  fourierdlem111  46790  fourierdlem112  46791  fourierdlem113  46792  fouriersw  46804  fouriercn  46805  ioorrnopnlem  46877  hspdifhsp  47189  hspmbllem2  47200  hspmbl  47202  iunhoiioolem  47248  smfresal  47361  smfpimbor1lem1  47371