Theorem ioossicc 13423

Description: An open interval is a subset of its closure. (Contributed by Paul Chapman, 18-Oct-2007.)

Assertion

Ref	Expression
ioossicc	⊢ (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵)

Proof of Theorem ioossicc

Dummy variables 𝑥 𝑤 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-ioo 13339	. 2 ⊢ (,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)})
2		df-icc 13342	. 2 ⊢ [,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)})
3		xrltle 13137	. 2 ⊢ ((𝐴 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) → (𝐴 < 𝑤 → 𝐴 ≤ 𝑤))
4		xrltle 13137	. 2 ⊢ ((𝑤 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝑤 < 𝐵 → 𝑤 ≤ 𝐵))
5	1, 2, 3, 4	ixxssixx 13349	1 ⊢ (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵)

Syntax hints:   ⊆ wss 3895  (class class class)co 7381   < clt 11202   ≤ cle 11203  (,)cioo 13335  [,]cicc 13338

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-8 2134  ax-9 2142  ax-10 2165  ax-11 2181  ax-12 2202  ax-ext 2724  ax-sep 5236  ax-nul 5246  ax-pow 5312  ax-pr 5380  ax-un 7703  ax-cnex 11115  ax-resscn 11116  ax-pre-lttri 11133  ax-pre-lttrn 11134

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-3or 1096  df-3an 1097  df-tru 1553  df-fal 1563  df-ex 1790  df-nf 1794  df-sb 2081  df-mo 2556  df-eu 2586  df-clab 2731  df-cleq 2744  df-clel 2827  df-nfc 2901  df-ne 2948  df-nel 3052  df-ral 3067  df-rex 3077  df-rab 3405  df-v 3446  df-sbc 3736  df-csb 3844  df-dif 3898  df-un 3900  df-in 3902  df-ss 3912  df-nul 4277  df-if 4471  df-pw 4547  df-sn 4573  df-pr 4575  df-op 4579  df-uni 4856  df-br 5091  df-opab 5153  df-mpt 5172  df-id 5531  df-po 5544  df-so 5545  df-xp 5642  df-rel 5643  df-cnv 5644  df-co 5645  df-dm 5646  df-rn 5647  df-res 5648  df-ima 5649  df-iota 6462  df-fun 6508  df-fn 6509  df-f 6510  df-f1 6511  df-fo 6512  df-f1o 6513  df-fv 6514  df-ov 7384  df-oprab 7385  df-mpo 7386  df-er 8662  df-en 8913  df-dom 8914  df-sdom 8915  df-pnf 11204  df-mnf 11205  df-xr 11206  df-ltxr 11207  df-le 11208  df-ioo 13339  df-icc 13342

This theorem is referenced by:  ioodisj  13472  iccntr  24851  ivth2  25486  ivthle  25487  ivthle2  25488  ovolioo  25599  uniiccvol  25611  itgioo  25847  rollelem  26020  rolle  26021  cmvth  26022  dvlip  26024  dvlipcn  26025  dvlip2  26026  c1liplem1  26027  dvle  26038  dvivthlem1  26039  dvne0  26042  lhop1lem  26044  dvcnvrelem1  26048  dvfsumle  26052  dvfsumge  26053  dvfsumabs  26054  dvfsumlem2  26058  ftc1a  26068  ftc1lem4  26070  ftc1lem5  26071  ftc1lem6  26072  ftc1  26073  ftc2  26075  itgparts  26078  itgsubstlem  26079  itgsubst  26080  itgpowd  26081  reeff1olem  26475  efcvx  26478  cos0pilt1  26563  tanord1  26568  logccv  26694  loglesqrt  26792  chordthm  26868  amgmlem  27020  lgamgulmlem2  27060  eliccioo  33058  xrge0mulc1cn  34182  omssubadd  34541  ftc2re  34839  fdvposlt  34840  fdvneggt  34841  fdvposle  34842  fdvnegge  34843  circlemeth  34881  logdivsqrle  34891  ivthALT  36633  iccioo01  37759  itg2gt0cn  38112  ftc1cnnclem  38128  ftc1cnnc  38129  ftc2nc  38139  areacirc  38150  lcmineqlem10  42593  lcmineqlem12  42595  lhe4.4ex1a  44843  chordthmALT  45446  iccnct  46055  limciccioolb  46135  limcicciooub  46149  icccncfext  46399  cncfiooicclem1  46405  cncfioobdlem  46408  cncfioobd  46409  itgsin0pilem1  46462  iblioosinexp  46465  itgsinexplem1  46466  itgsinexp  46467  ditgeqiooicc  46472  itgcoscmulx  46481  ibliooicc  46483  itgsincmulx  46486  itgsubsticclem  46487  itgioocnicc  46489  iblcncfioo  46490  itgsbtaddcnst  46494  dirkeritg  46614  fourierdlem20  46639  fourierdlem38  46657  fourierdlem39  46658  fourierdlem46  46664  fourierdlem62  46680  fourierdlem68  46686  fourierdlem69  46687  fourierdlem70  46688  fourierdlem72  46690  fourierdlem73  46691  fourierdlem74  46692  fourierdlem75  46693  fourierdlem76  46694  fourierdlem80  46698  fourierdlem81  46699  fourierdlem82  46700  fourierdlem83  46701  fourierdlem84  46702  fourierdlem85  46703  fourierdlem88  46706  fourierdlem92  46710  fourierdlem93  46711  fourierdlem100  46718  fourierdlem101  46719  fourierdlem103  46721  fourierdlem104  46722  fourierdlem107  46725  fourierdlem111  46729  fourierdlem112  46730  sqwvfoura  46740  sqwvfourb  46741  etransclem18  46764  etransclem46  46792  hoicvrrex  47068  iooii  49477