Theorem ioossre 13568

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

This proof depends on syntax axioms:   ⊆ wss 3900  (class class class)co 7446  ℝcr 11229  (,)cioo 13506

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5253  ax-nul 5264  ax-pow 5332  ax-pr 5396  ax-un 7778  ax-cnex 11286  ax-resscn 11287  ax-pre-lttri 11304  ax-pre-lttrn 11305

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3066  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-iun 4956  df-br 5107  df-opab 5172  df-mpt 5191  df-id 5551  df-po 5564  df-so 5565  df-xp 5662  df-rel 5663  df-cnv 5664  df-co 5665  df-dm 5666  df-rn 5667  df-res 5668  df-ima 5669  df-iota 6515  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-ov 7449  df-oprab 7450  df-mpo 7451  df-1st 8028  df-2nd 8029  df-er 8748  df-en 9005  df-dom 9006  df-sdom 9007  df-pnf 11375  df-mnf 11376  df-xr 11377  df-ltxr 11378  df-le 11379  df-ioo 13510

This theorem is used by:  ioosscn  13569  ioof  13608  difreicc  13645  icopnfcld  25119  ioombl1  25916  ioorcl2  25926  uniioombllem2  25937  uniioombllem3a  25938  uniioombllem3  25939  uniioombllem4  25940  uniioombllem6  25942  ismbf3d  26008  itgsplitioo  26191  ditgeq3  26203  dvmptresicc  26269  dvferm1lem  26337  dvferm2lem  26339  dvferm  26341  dvlip  26346  dvlipcn  26347  dvle  26360  dvivthlem1  26361  dvivth  26363  lhop1lem  26366  lhop1  26367  lhop2  26368  lhop  26369  dvfsumle  26374  dvfsumge  26375  dvfsumlem1  26379  dvfsumlem2  26380  dvfsumlem3  26381  dvfsumlem4  26382  dvfsumrlimge0  26383  dvfsumrlim  26384  dvfsumrlim2  26385  dvfsum2  26387  ftc1a  26390  ftc1cn  26396  ftc2  26397  itgsubstlem  26401  itgsubst  26402  itgpowd  26403  efcvx  26809  pige3ALT  26881  tanord  26899  divlogrlim  26996  logccv  27024  atantan  27284  amgmlem  27350  vmalogdivsum2  27898  2vmadivsumlem  27900  chpdifbndlem1  27913  selberg3lem1  27917  selberg4lem1  27920  selberg4  27921  selberg3r  27929  selberg4r  27930  selberg34r  27931  pntrlog2bndlem2  27938  pntrlog2bndlem3  27939  pntrlog2bndlem4  27940  pntrlog2bndlem5  27941  pntrlog2bndlem6  27943  pntrlog2bnd  27944  pntpbnd1a  27945  pntpbnd1  27946  pntpbnd2  27947  pntibndlem2a  27950  pntibndlem2  27951  pntibndlem3  27952  pntlemd  27954  pnt  27974  padicabv  27990  cnre2csqima  34626  ftc2re  35310  fdvposlt  35311  fdvposle  35313  itgexpif  35318  circlemeth  35352  circlemethnat  35353  circlevma  35354  circlemethhgt  35355  ioosconn  36192  iccllysconn  36195  itg2gt0cn  38798  itggt0cn  38813  ftc1cnnclem  38814  ftc1cnnc  38815  ftc1anclem8  38823  ftc2nc  38825  dvreasin  38829  dvreacos  38830  areacirclem1  38831  areacirc  38836  aks4d1p1p6  43326  aks4d1p1p5  43328  ioontr  46738  iooshift  46749  ioonct  46764  iooiinicc  46769  icomnfinre  46779  iooiinioc  46783  islptre  46846  lptioo2  46858  lptioo1  46859  limcresiooub  46867  limcresioolb  46868  limcleqr  46869  lptioo2cn  46870  lptioo1cn  46871  limclner  46876  limclr  46880  icccncfext  47112  cncfiooicclem1  47118  dvresioo  47146  dvbdfbdioolem1  47153  dvbdfbdioolem2  47154  ioodvbdlimc1lem1  47156  ioodvbdlimc1lem2  47157  ioodvbdlimc2lem  47159  itgsin0pilem1  47175  itgcoscmulx  47194  itgiccshift  47205  itgperiod  47206  itgsbtaddcnst  47207  dirkercncflem2  47329  dirkercncflem3  47330  dirkercncflem4  47331  fourierdlem16  47348  fourierdlem21  47353  fourierdlem22  47354  fourierdlem28  47360  fourierdlem48  47379  fourierdlem49  47380  fourierdlem50  47381  fourierdlem56  47387  fourierdlem57  47388  fourierdlem59  47390  fourierdlem60  47391  fourierdlem61  47392  fourierdlem65  47396  fourierdlem72  47403  fourierdlem74  47405  fourierdlem75  47406  fourierdlem76  47407  fourierdlem80  47411  fourierdlem81  47412  fourierdlem83  47414  fourierdlem84  47415  fourierdlem85  47416  fourierdlem88  47419  fourierdlem89  47420  fourierdlem90  47421  fourierdlem91  47422  fourierdlem92  47423  fourierdlem94  47425  fourierdlem95  47426  fourierdlem97  47428  fourierdlem101  47432  fourierdlem103  47434  fourierdlem104  47435  fourierdlem111  47442  fourierdlem112  47443  fourierdlem113  47444  fouriersw  47456  fouriercn  47457  ioorrnopnlem  47529  hspdifhsp  47841  hspmbllem2  47852  hspmbl  47854  iunhoiioolem  47900  smfresal  48013  smfpimbor1lem1  48023