Theorem ioossicc 13377

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 13293	. 2 ⊢ (,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)})
2		df-icc 13296	. 2 ⊢ [,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)})
3		xrltle 13091	. 2 ⊢ ((𝐴 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) → (𝐴 < 𝑤 → 𝐴 ≤ 𝑤))
4		xrltle 13091	. 2 ⊢ ((𝑤 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝑤 < 𝐵 → 𝑤 ≤ 𝐵))
5	1, 2, 3, 4	ixxssixx 13303	1 ⊢ (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵)

Syntax hints:   ⊆ wss 3890  (class class class)co 7360   < clt 11170   ≤ cle 11171  (,)cioo 13289  [,]cicc 13292

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pow 5302  ax-pr 5370  ax-un 7682  ax-cnex 11085  ax-resscn 11086  ax-pre-lttri 11103  ax-pre-lttrn 11104

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5519  df-po 5532  df-so 5533  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-ov 7363  df-oprab 7364  df-mpo 7365  df-er 8636  df-en 8887  df-dom 8888  df-sdom 8889  df-pnf 11172  df-mnf 11173  df-xr 11174  df-ltxr 11175  df-le 11176  df-ioo 13293  df-icc 13296

This theorem is referenced by:  ioodisj  13426  iccntr  24797  ivth2  25432  ivthle  25433  ivthle2  25434  ovolioo  25545  uniiccvol  25557  itgioo  25793  rollelem  25966  rolle  25967  cmvth  25968  dvlip  25970  dvlipcn  25971  dvlip2  25972  c1liplem1  25973  dvle  25984  dvivthlem1  25985  dvne0  25988  lhop1lem  25990  dvcnvrelem1  25994  dvfsumle  25998  dvfsumge  25999  dvfsumabs  26000  dvfsumlem2  26004  ftc1a  26014  ftc1lem4  26016  ftc1lem5  26017  ftc1lem6  26018  ftc1  26019  ftc2  26021  itgparts  26024  itgsubstlem  26025  itgsubst  26026  itgpowd  26027  reeff1olem  26424  efcvx  26427  cos0pilt1  26509  tanord1  26514  logccv  26640  loglesqrt  26738  chordthm  26814  amgmlem  26967  lgamgulmlem2  27007  eliccioo  33005  xrge0mulc1cn  34101  omssubadd  34460  ftc2re  34758  fdvposlt  34759  fdvneggt  34760  fdvposle  34761  fdvnegge  34762  circlemeth  34800  logdivsqrle  34810  ivthALT  36533  iccioo01  37657  itg2gt0cn  38010  ftc1cnnclem  38026  ftc1cnnc  38027  ftc2nc  38037  areacirc  38048  lcmineqlem10  42491  lcmineqlem12  42493  lhe4.4ex1a  44774  chordthmALT  45377  iccnct  45989  limciccioolb  46069  limcicciooub  46083  icccncfext  46333  cncfiooicclem1  46339  cncfioobdlem  46342  cncfioobd  46343  itgsin0pilem1  46396  iblioosinexp  46399  itgsinexplem1  46400  itgsinexp  46401  ditgeqiooicc  46406  itgcoscmulx  46415  ibliooicc  46417  itgsincmulx  46420  itgsubsticclem  46421  itgioocnicc  46423  iblcncfioo  46424  itgsbtaddcnst  46428  dirkeritg  46548  fourierdlem20  46573  fourierdlem38  46591  fourierdlem39  46592  fourierdlem46  46598  fourierdlem62  46614  fourierdlem68  46620  fourierdlem69  46621  fourierdlem70  46622  fourierdlem72  46624  fourierdlem73  46625  fourierdlem74  46626  fourierdlem75  46627  fourierdlem76  46628  fourierdlem80  46632  fourierdlem81  46633  fourierdlem82  46634  fourierdlem83  46635  fourierdlem84  46636  fourierdlem85  46637  fourierdlem88  46640  fourierdlem92  46644  fourierdlem93  46645  fourierdlem100  46652  fourierdlem101  46653  fourierdlem103  46655  fourierdlem104  46656  fourierdlem107  46659  fourierdlem111  46663  fourierdlem112  46664  sqwvfoura  46674  sqwvfourb  46675  etransclem18  46698  etransclem46  46726  hoicvrrex  47002  iooii  49405