Theorem ioossre 13542

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

This proof depends on syntax axioms:   ⊆ wss 3895  (class class class)co 7421  ℝcr 11203  (,)cioo 13480

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7752  ax-cnex 11260  ax-resscn 11261  ax-pre-lttri 11278  ax-pre-lttrn 11279

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5545  df-po 5558  df-so 5559  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-iota 6494  df-fun 6541  df-fn 6542  df-f 6543  df-f1 6544  df-fo 6545  df-f1o 6546  df-fv 6547  df-ov 7424  df-oprab 7425  df-mpo 7426  df-1st 8002  df-2nd 8003  df-er 8721  df-en 8978  df-dom 8979  df-sdom 8980  df-pnf 11349  df-mnf 11350  df-xr 11351  df-ltxr 11352  df-le 11353  df-ioo 13484

This theorem is used by:  ioosscn  13543  ioof  13582  difreicc  13619  icopnfcld  25092  ioombl1  25889  ioorcl2  25899  uniioombllem2  25910  uniioombllem3a  25911  uniioombllem3  25912  uniioombllem4  25913  uniioombllem6  25915  ismbf3d  25981  itgsplitioo  26164  ditgeq3  26176  dvmptresicc  26242  dvferm1lem  26310  dvferm2lem  26312  dvferm  26314  dvlip  26319  dvlipcn  26320  dvle  26333  dvivthlem1  26334  dvivth  26336  lhop1lem  26339  lhop1  26340  lhop2  26341  lhop  26342  dvfsumle  26347  dvfsumge  26348  dvfsumlem1  26352  dvfsumlem2  26353  dvfsumlem3  26354  dvfsumlem4  26355  dvfsumrlimge0  26356  dvfsumrlim  26357  dvfsumrlim2  26358  dvfsum2  26360  ftc1a  26363  ftc1cn  26369  ftc2  26370  itgsubstlem  26374  itgsubst  26375  itgpowd  26376  efcvx  26782  pige3ALT  26854  tanord  26872  divlogrlim  26969  logccv  26997  atantan  27257  amgmlem  27323  vmalogdivsum2  27871  2vmadivsumlem  27873  chpdifbndlem1  27886  selberg3lem1  27890  selberg4lem1  27893  selberg4  27894  selberg3r  27902  selberg4r  27903  selberg34r  27904  pntrlog2bndlem2  27911  pntrlog2bndlem3  27912  pntrlog2bndlem4  27913  pntrlog2bndlem5  27914  pntrlog2bndlem6  27916  pntrlog2bnd  27917  pntpbnd1a  27918  pntpbnd1  27919  pntpbnd2  27920  pntibndlem2a  27923  pntibndlem2  27924  pntibndlem3  27925  pntlemd  27927  pnt  27947  padicabv  27963  cnre2csqima  34590  ftc2re  35274  fdvposlt  35275  fdvposle  35277  itgexpif  35282  circlemeth  35316  circlemethnat  35317  circlevma  35318  circlemethhgt  35319  ioosconn  36099  iccllysconn  36102  itg2gt0cn  38687  itggt0cn  38702  ftc1cnnclem  38703  ftc1cnnc  38704  ftc1anclem8  38712  ftc2nc  38714  dvreasin  38718  dvreacos  38719  areacirclem1  38720  areacirc  38725  aks4d1p1p6  43217  aks4d1p1p5  43219  ioontr  46617  iooshift  46628  ioonct  46643  iooiinicc  46648  icomnfinre  46658  iooiinioc  46662  islptre  46725  lptioo2  46737  lptioo1  46738  limcresiooub  46746  limcresioolb  46747  limcleqr  46748  lptioo2cn  46749  lptioo1cn  46750  limclner  46755  limclr  46759  icccncfext  46991  cncfiooicclem1  46997  dvresioo  47025  dvbdfbdioolem1  47032  dvbdfbdioolem2  47033  ioodvbdlimc1lem1  47035  ioodvbdlimc1lem2  47036  ioodvbdlimc2lem  47038  itgsin0pilem1  47054  itgcoscmulx  47073  itgiccshift  47084  itgperiod  47085  itgsbtaddcnst  47086  dirkercncflem2  47208  dirkercncflem3  47209  dirkercncflem4  47210  fourierdlem16  47227  fourierdlem21  47232  fourierdlem22  47233  fourierdlem28  47239  fourierdlem48  47258  fourierdlem49  47259  fourierdlem50  47260  fourierdlem56  47266  fourierdlem57  47267  fourierdlem59  47269  fourierdlem60  47270  fourierdlem61  47271  fourierdlem65  47275  fourierdlem72  47282  fourierdlem74  47284  fourierdlem75  47285  fourierdlem76  47286  fourierdlem80  47290  fourierdlem81  47291  fourierdlem83  47293  fourierdlem84  47294  fourierdlem85  47295  fourierdlem88  47298  fourierdlem89  47299  fourierdlem90  47300  fourierdlem91  47301  fourierdlem92  47302  fourierdlem94  47304  fourierdlem95  47305  fourierdlem97  47307  fourierdlem101  47311  fourierdlem103  47313  fourierdlem104  47314  fourierdlem111  47321  fourierdlem112  47322  fourierdlem113  47323  fouriersw  47335  fouriercn  47336  ioorrnopnlem  47408  hspdifhsp  47720  hspmbllem2  47731  hspmbl  47733  iunhoiioolem  47779  smfresal  47892  smfpimbor1lem1  47902