Theorem ioossre 13409

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

Syntax hints:   ⊆ wss 3944  (class class class)co 7414  ℝcr 11129  (,)cioo 13348

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2164  ax-ext 2698  ax-sep 5293  ax-nul 5300  ax-pow 5359  ax-pr 5423  ax-un 7734  ax-cnex 11186  ax-resscn 11187  ax-pre-lttri 11204  ax-pre-lttrn 11205

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2936  df-nel 3042  df-ral 3057  df-rex 3066  df-rab 3428  df-v 3471  df-sbc 3775  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-iun 4993  df-br 5143  df-opab 5205  df-mpt 5226  df-id 5570  df-po 5584  df-so 5585  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-ov 7417  df-oprab 7418  df-mpo 7419  df-1st 7987  df-2nd 7988  df-er 8718  df-en 8956  df-dom 8957  df-sdom 8958  df-pnf 11272  df-mnf 11273  df-xr 11274  df-ltxr 11275  df-le 11276  df-ioo 13352

This theorem is referenced by:  ioosscn  13410  ioof  13448  difreicc  13485  icopnfcld  24671  ioombl1  25478  ioorcl2  25488  uniioombllem2  25499  uniioombllem3a  25500  uniioombllem3  25501  uniioombllem4  25502  uniioombllem6  25504  ismbf3d  25570  itgsplitioo  25754  ditgeq3  25766  dvmptresicc  25832  dvferm1lem  25903  dvferm2lem  25905  dvferm  25907  dvlip  25913  dvlipcn  25914  dvle  25927  dvivthlem1  25928  dvivth  25930  lhop1lem  25933  lhop1  25934  lhop2  25935  lhop  25936  dvfsumle  25941  dvfsumleOLD  25942  dvfsumge  25943  dvfsumlem1  25947  dvfsumlem2  25948  dvfsumlem2OLD  25949  dvfsumlem3  25950  dvfsumlem4  25951  dvfsumrlimge0  25952  dvfsumrlim  25953  dvfsumrlim2  25954  dvfsum2  25956  ftc1a  25959  ftc1cn  25965  ftc2  25966  itgsubstlem  25970  itgsubst  25971  itgpowd  25972  efcvx  26373  pige3ALT  26441  tanord  26459  divlogrlim  26556  logccv  26584  atantan  26842  amgmlem  26909  vmalogdivsum2  27458  2vmadivsumlem  27460  chpdifbndlem1  27473  selberg3lem1  27477  selberg4lem1  27480  selberg4  27481  selberg3r  27489  selberg4r  27490  selberg34r  27491  pntrlog2bndlem2  27498  pntrlog2bndlem3  27499  pntrlog2bndlem4  27500  pntrlog2bndlem5  27501  pntrlog2bndlem6  27503  pntrlog2bnd  27504  pntpbnd1a  27505  pntpbnd1  27506  pntpbnd2  27507  pntibndlem2a  27510  pntibndlem2  27511  pntibndlem3  27512  pntlemd  27514  pnt  27534  padicabv  27550  cnre2csqima  33448  ftc2re  34166  fdvposlt  34167  fdvposle  34169  itgexpif  34174  circlemeth  34208  circlemethnat  34209  circlevma  34210  circlemethhgt  34211  ioosconn  34793  iccllysconn  34796  itg2gt0cn  37083  itggt0cn  37098  ftc1cnnclem  37099  ftc1cnnc  37100  ftc1anclem8  37108  ftc2nc  37110  dvreasin  37114  dvreacos  37115  areacirclem1  37116  areacirc  37121  aks4d1p1p6  41481  aks4d1p1p5  41483  ioontr  44819  iooshift  44830  ioonct  44845  iooiinicc  44850  icomnfinre  44860  iooiinioc  44864  islptre  44930  lptioo2  44942  lptioo1  44943  limcresiooub  44953  limcresioolb  44954  limcleqr  44955  lptioo2cn  44956  lptioo1cn  44957  limclner  44962  limclr  44966  icccncfext  45198  cncfiooicclem1  45204  dvresioo  45232  dvbdfbdioolem1  45239  dvbdfbdioolem2  45240  ioodvbdlimc1lem1  45242  ioodvbdlimc1lem2  45243  ioodvbdlimc2lem  45245  itgsin0pilem1  45261  itgcoscmulx  45280  itgiccshift  45291  itgperiod  45292  itgsbtaddcnst  45293  dirkercncflem2  45415  dirkercncflem3  45416  dirkercncflem4  45417  fourierdlem16  45434  fourierdlem21  45439  fourierdlem22  45440  fourierdlem28  45446  fourierdlem48  45465  fourierdlem49  45466  fourierdlem50  45467  fourierdlem56  45473  fourierdlem57  45474  fourierdlem59  45476  fourierdlem60  45477  fourierdlem61  45478  fourierdlem65  45482  fourierdlem72  45489  fourierdlem74  45491  fourierdlem75  45492  fourierdlem76  45493  fourierdlem80  45497  fourierdlem81  45498  fourierdlem83  45500  fourierdlem84  45501  fourierdlem85  45502  fourierdlem88  45505  fourierdlem89  45506  fourierdlem90  45507  fourierdlem91  45508  fourierdlem92  45509  fourierdlem94  45511  fourierdlem95  45512  fourierdlem97  45514  fourierdlem101  45518  fourierdlem103  45520  fourierdlem104  45521  fourierdlem111  45528  fourierdlem112  45529  fourierdlem113  45530  fouriersw  45542  fouriercn  45543  ioorrnopnlem  45615  hspdifhsp  45927  hspmbllem2  45938  hspmbl  45940  iunhoiioolem  45986  smfresal  46099  smfpimbor1lem1  46109