Theorem ioossre 13335

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

Syntax hints:   ⊆ wss 3903  (class class class)co 7368  ℝcr 11037  (,)cioo 13273

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pow 5312  ax-pr 5379  ax-un 7690  ax-cnex 11094  ax-resscn 11095  ax-pre-lttri 11112  ax-pre-lttrn 11113

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-iun 4950  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-po 5540  df-so 5541  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-ov 7371  df-oprab 7372  df-mpo 7373  df-1st 7943  df-2nd 7944  df-er 8645  df-en 8896  df-dom 8897  df-sdom 8898  df-pnf 11180  df-mnf 11181  df-xr 11182  df-ltxr 11183  df-le 11184  df-ioo 13277

This theorem is referenced by:  ioosscn  13336  ioof  13375  difreicc  13412  icopnfcld  24723  ioombl1  25531  ioorcl2  25541  uniioombllem2  25552  uniioombllem3a  25553  uniioombllem3  25554  uniioombllem4  25555  uniioombllem6  25557  ismbf3d  25623  itgsplitioo  25807  ditgeq3  25819  dvmptresicc  25885  dvferm1lem  25956  dvferm2lem  25958  dvferm  25960  dvlip  25966  dvlipcn  25967  dvle  25980  dvivthlem1  25981  dvivth  25983  lhop1lem  25986  lhop1  25987  lhop2  25988  lhop  25989  dvfsumle  25994  dvfsumleOLD  25995  dvfsumge  25996  dvfsumlem1  26000  dvfsumlem2  26001  dvfsumlem2OLD  26002  dvfsumlem3  26003  dvfsumlem4  26004  dvfsumrlimge0  26005  dvfsumrlim  26006  dvfsumrlim2  26007  dvfsum2  26009  ftc1a  26012  ftc1cn  26018  ftc2  26019  itgsubstlem  26023  itgsubst  26024  itgpowd  26025  efcvx  26427  pige3ALT  26497  tanord  26515  divlogrlim  26612  logccv  26640  atantan  26901  amgmlem  26968  vmalogdivsum2  27517  2vmadivsumlem  27519  chpdifbndlem1  27532  selberg3lem1  27536  selberg4lem1  27539  selberg4  27540  selberg3r  27548  selberg4r  27549  selberg34r  27550  pntrlog2bndlem2  27557  pntrlog2bndlem3  27558  pntrlog2bndlem4  27559  pntrlog2bndlem5  27560  pntrlog2bndlem6  27562  pntrlog2bnd  27563  pntpbnd1a  27564  pntpbnd1  27565  pntpbnd2  27566  pntibndlem2a  27569  pntibndlem2  27570  pntibndlem3  27571  pntlemd  27573  pnt  27593  padicabv  27609  cnre2csqima  34088  ftc2re  34775  fdvposlt  34776  fdvposle  34778  itgexpif  34783  circlemeth  34817  circlemethnat  34818  circlevma  34819  circlemethhgt  34820  ioosconn  35460  iccllysconn  35463  itg2gt0cn  37923  itggt0cn  37938  ftc1cnnclem  37939  ftc1cnnc  37940  ftc1anclem8  37948  ftc2nc  37950  dvreasin  37954  dvreacos  37955  areacirclem1  37956  areacirc  37961  aks4d1p1p6  42440  aks4d1p1p5  42442  ioontr  45868  iooshift  45879  ioonct  45894  iooiinicc  45899  icomnfinre  45909  iooiinioc  45913  islptre  45976  lptioo2  45988  lptioo1  45989  limcresiooub  45997  limcresioolb  45998  limcleqr  45999  lptioo2cn  46000  lptioo1cn  46001  limclner  46006  limclr  46010  icccncfext  46242  cncfiooicclem1  46248  dvresioo  46276  dvbdfbdioolem1  46283  dvbdfbdioolem2  46284  ioodvbdlimc1lem1  46286  ioodvbdlimc1lem2  46287  ioodvbdlimc2lem  46289  itgsin0pilem1  46305  itgcoscmulx  46324  itgiccshift  46335  itgperiod  46336  itgsbtaddcnst  46337  dirkercncflem2  46459  dirkercncflem3  46460  dirkercncflem4  46461  fourierdlem16  46478  fourierdlem21  46483  fourierdlem22  46484  fourierdlem28  46490  fourierdlem48  46509  fourierdlem49  46510  fourierdlem50  46511  fourierdlem56  46517  fourierdlem57  46518  fourierdlem59  46520  fourierdlem60  46521  fourierdlem61  46522  fourierdlem65  46526  fourierdlem72  46533  fourierdlem74  46535  fourierdlem75  46536  fourierdlem76  46537  fourierdlem80  46541  fourierdlem81  46542  fourierdlem83  46544  fourierdlem84  46545  fourierdlem85  46546  fourierdlem88  46549  fourierdlem89  46550  fourierdlem90  46551  fourierdlem91  46552  fourierdlem92  46553  fourierdlem94  46555  fourierdlem95  46556  fourierdlem97  46558  fourierdlem101  46562  fourierdlem103  46564  fourierdlem104  46565  fourierdlem111  46572  fourierdlem112  46573  fourierdlem113  46574  fouriersw  46586  fouriercn  46587  ioorrnopnlem  46659  hspdifhsp  46971  hspmbllem2  46982  hspmbl  46984  iunhoiioolem  47030  smfresal  47143  smfpimbor1lem1  47153