Theorem ioossre 13464

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

This proof depends on syntax axioms:   ⊆ wss 3902  (class class class)co 7417  ℝcr 11127  (,)cioo 13402

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pow 5334  ax-pr 5402  ax-un 7740  ax-cnex 11184  ax-resscn 11185  ax-pre-lttri 11202  ax-pre-lttrn 11203

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 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-nel 3064  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-iun 4956  df-br 5108  df-opab 5172  df-mpt 5191  df-id 5554  df-po 5567  df-so 5568  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-ov 7420  df-oprab 7421  df-mpo 7422  df-1st 7990  df-2nd 7991  df-er 8700  df-en 8957  df-dom 8958  df-sdom 8959  df-pnf 11273  df-mnf 11274  df-xr 11275  df-ltxr 11276  df-le 11277  df-ioo 13406

This theorem is used by:  ioosscn  13465  ioof  13504  difreicc  13541  icopnfcld  24999  ioombl1  25796  ioorcl2  25806  uniioombllem2  25817  uniioombllem3a  25818  uniioombllem3  25819  uniioombllem4  25820  uniioombllem6  25822  ismbf3d  25888  itgsplitioo  26072  ditgeq3  26084  dvmptresicc  26150  dvferm1lem  26218  dvferm2lem  26220  dvferm  26222  dvlip  26227  dvlipcn  26228  dvle  26241  dvivthlem1  26242  dvivth  26244  lhop1lem  26247  lhop1  26248  lhop2  26249  lhop  26250  dvfsumle  26255  dvfsumge  26256  dvfsumlem1  26260  dvfsumlem2  26261  dvfsumlem3  26262  dvfsumlem4  26263  dvfsumrlimge0  26264  dvfsumrlim  26265  dvfsumrlim2  26266  dvfsum2  26268  ftc1a  26271  ftc1cn  26277  ftc2  26278  itgsubstlem  26282  itgsubst  26283  itgpowd  26284  efcvx  26692  pige3ALT  26765  tanord  26783  divlogrlim  26880  logccv  26908  atantan  27168  amgmlem  27234  vmalogdivsum2  27782  2vmadivsumlem  27784  chpdifbndlem1  27797  selberg3lem1  27801  selberg4lem1  27804  selberg4  27805  selberg3r  27813  selberg4r  27814  selberg34r  27815  pntrlog2bndlem2  27822  pntrlog2bndlem3  27823  pntrlog2bndlem4  27824  pntrlog2bndlem5  27825  pntrlog2bndlem6  27827  pntrlog2bnd  27828  pntpbnd1a  27829  pntpbnd1  27830  pntpbnd2  27831  pntibndlem2a  27834  pntibndlem2  27835  pntibndlem3  27836  pntlemd  27838  pnt  27858  padicabv  27874  cnre2csqima  34429  ftc2re  35114  fdvposlt  35115  fdvposle  35117  itgexpif  35122  circlemeth  35156  circlemethnat  35157  circlevma  35158  circlemethhgt  35159  ioosconn  35834  iccllysconn  35837  itg2gt0cn  38432  itggt0cn  38447  ftc1cnnclem  38448  ftc1cnnc  38449  ftc1anclem8  38457  ftc2nc  38459  dvreasin  38463  dvreacos  38464  areacirclem1  38465  areacirc  38470  aks4d1p1p6  42947  aks4d1p1p5  42949  ioontr  46349  iooshift  46360  ioonct  46375  iooiinicc  46380  icomnfinre  46390  iooiinioc  46394  islptre  46457  lptioo2  46469  lptioo1  46470  limcresiooub  46478  limcresioolb  46479  limcleqr  46480  lptioo2cn  46481  lptioo1cn  46482  limclner  46487  limclr  46491  icccncfext  46723  cncfiooicclem1  46729  dvresioo  46757  dvbdfbdioolem1  46764  dvbdfbdioolem2  46765  ioodvbdlimc1lem1  46767  ioodvbdlimc1lem2  46768  ioodvbdlimc2lem  46770  itgsin0pilem1  46786  itgcoscmulx  46805  itgiccshift  46816  itgperiod  46817  itgsbtaddcnst  46818  dirkercncflem2  46940  dirkercncflem3  46941  dirkercncflem4  46942  fourierdlem16  46959  fourierdlem21  46964  fourierdlem22  46965  fourierdlem28  46971  fourierdlem48  46990  fourierdlem49  46991  fourierdlem50  46992  fourierdlem56  46998  fourierdlem57  46999  fourierdlem59  47001  fourierdlem60  47002  fourierdlem61  47003  fourierdlem65  47007  fourierdlem72  47014  fourierdlem74  47016  fourierdlem75  47017  fourierdlem76  47018  fourierdlem80  47022  fourierdlem81  47023  fourierdlem83  47025  fourierdlem84  47026  fourierdlem85  47027  fourierdlem88  47030  fourierdlem89  47031  fourierdlem90  47032  fourierdlem91  47033  fourierdlem92  47034  fourierdlem94  47036  fourierdlem95  47037  fourierdlem97  47039  fourierdlem101  47043  fourierdlem103  47045  fourierdlem104  47046  fourierdlem111  47053  fourierdlem112  47054  fourierdlem113  47055  fouriersw  47067  fouriercn  47068  ioorrnopnlem  47140  hspdifhsp  47452  hspmbllem2  47463  hspmbl  47465  iunhoiioolem  47511  smfresal  47624  smfpimbor1lem1  47634