Theorem ioossre 13381

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

Syntax hints:   ⊆ wss 3947  (class class class)co 7405  ℝcr 11105  (,)cioo 13320

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721  ax-cnex 11162  ax-resscn 11163  ax-pre-lttri 11180  ax-pre-lttrn 11181

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-po 5587  df-so 5588  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-ov 7408  df-oprab 7409  df-mpo 7410  df-1st 7971  df-2nd 7972  df-er 8699  df-en 8936  df-dom 8937  df-sdom 8938  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-ioo 13324

This theorem is referenced by:  ioosscn  13382  ioof  13420  difreicc  13457  icopnfcld  24275  ioombl1  25070  ioorcl2  25080  uniioombllem2  25091  uniioombllem3a  25092  uniioombllem3  25093  uniioombllem4  25094  uniioombllem6  25096  ismbf3d  25162  itgsplitioo  25346  ditgeq3  25358  dvmptresicc  25424  dvferm1lem  25492  dvferm2lem  25494  dvferm  25496  dvlip  25501  dvlipcn  25502  dvle  25515  dvivthlem1  25516  dvivth  25518  lhop1lem  25521  lhop1  25522  lhop2  25523  lhop  25524  dvfsumle  25529  dvfsumge  25530  dvfsumlem1  25534  dvfsumlem2  25535  dvfsumlem3  25536  dvfsumlem4  25537  dvfsumrlimge0  25538  dvfsumrlim  25539  dvfsumrlim2  25540  dvfsum2  25542  ftc1a  25545  ftc1cn  25551  ftc2  25552  itgsubstlem  25556  itgsubst  25557  itgpowd  25558  efcvx  25952  pige3ALT  26020  tanord  26038  divlogrlim  26134  logccv  26162  atantan  26417  amgmlem  26483  vmalogdivsum2  27030  2vmadivsumlem  27032  chpdifbndlem1  27045  selberg3lem1  27049  selberg4lem1  27052  selberg4  27053  selberg3r  27061  selberg4r  27062  selberg34r  27063  pntrlog2bndlem2  27070  pntrlog2bndlem3  27071  pntrlog2bndlem4  27072  pntrlog2bndlem5  27073  pntrlog2bndlem6  27075  pntrlog2bnd  27076  pntpbnd1a  27077  pntpbnd1  27078  pntpbnd2  27079  pntibndlem2a  27082  pntibndlem2  27083  pntibndlem3  27084  pntlemd  27086  pnt  27106  padicabv  27122  cnre2csqima  32879  ftc2re  33598  fdvposlt  33599  fdvposle  33601  itgexpif  33606  circlemeth  33640  circlemethnat  33641  circlevma  33642  circlemethhgt  33643  ioosconn  34226  iccllysconn  34229  gg-dvfsumle  35170  gg-dvfsumlem2  35171  itg2gt0cn  36531  itggt0cn  36546  ftc1cnnclem  36547  ftc1cnnc  36548  ftc1anclem8  36556  ftc2nc  36558  dvreasin  36562  dvreacos  36563  areacirclem1  36564  areacirc  36569  aks4d1p1p6  40926  aks4d1p1p5  40928  ioontr  44210  iooshift  44221  ioonct  44236  iooiinicc  44241  icomnfinre  44251  iooiinioc  44255  islptre  44321  lptioo2  44333  lptioo1  44334  limcresiooub  44344  limcresioolb  44345  limcleqr  44346  lptioo2cn  44347  lptioo1cn  44348  limclner  44353  limclr  44357  icccncfext  44589  cncfiooicclem1  44595  dvresioo  44623  dvbdfbdioolem1  44630  dvbdfbdioolem2  44631  ioodvbdlimc1lem1  44633  ioodvbdlimc1lem2  44634  ioodvbdlimc2lem  44636  itgsin0pilem1  44652  itgcoscmulx  44671  itgiccshift  44682  itgperiod  44683  itgsbtaddcnst  44684  dirkercncflem2  44806  dirkercncflem3  44807  dirkercncflem4  44808  fourierdlem16  44825  fourierdlem21  44830  fourierdlem22  44831  fourierdlem28  44837  fourierdlem48  44856  fourierdlem49  44857  fourierdlem50  44858  fourierdlem56  44864  fourierdlem57  44865  fourierdlem59  44867  fourierdlem60  44868  fourierdlem61  44869  fourierdlem65  44873  fourierdlem72  44880  fourierdlem74  44882  fourierdlem75  44883  fourierdlem76  44884  fourierdlem80  44888  fourierdlem81  44889  fourierdlem83  44891  fourierdlem84  44892  fourierdlem85  44893  fourierdlem88  44896  fourierdlem89  44897  fourierdlem90  44898  fourierdlem91  44899  fourierdlem92  44900  fourierdlem94  44902  fourierdlem95  44903  fourierdlem97  44905  fourierdlem101  44909  fourierdlem103  44911  fourierdlem104  44912  fourierdlem111  44919  fourierdlem112  44920  fourierdlem113  44921  fouriersw  44933  fouriercn  44934  ioorrnopnlem  45006  hspdifhsp  45318  hspmbllem2  45329  hspmbl  45331  iunhoiioolem  45377  smfresal  45490  smfpimbor1lem1  45500