Theorem ioossicc 13174

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

Syntax hints:   ⊆ wss 3888  (class class class)co 7284   < clt 11018   ≤ cle 11019  (,)cioo 13088  [,]cicc 13091

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710  ax-sep 5224  ax-nul 5231  ax-pow 5289  ax-pr 5353  ax-un 7597  ax-cnex 10936  ax-resscn 10937  ax-pre-lttri 10954  ax-pre-lttrn 10955

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3435  df-sbc 3718  df-csb 3834  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-pw 4536  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-br 5076  df-opab 5138  df-mpt 5159  df-id 5490  df-po 5504  df-so 5505  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-iota 6395  df-fun 6439  df-fn 6440  df-f 6441  df-f1 6442  df-fo 6443  df-f1o 6444  df-fv 6445  df-ov 7287  df-oprab 7288  df-mpo 7289  df-er 8507  df-en 8743  df-dom 8744  df-sdom 8745  df-pnf 11020  df-mnf 11021  df-xr 11022  df-ltxr 11023  df-le 11024  df-ioo 13092  df-icc 13095

This theorem is referenced by:  ioodisj  13223  iccntr  23993  ivth2  24628  ivthle  24629  ivthle2  24630  ovolioo  24741  uniiccvol  24753  itgioo  24989  rollelem  25162  rolle  25163  cmvth  25164  dvlip  25166  dvlipcn  25167  dvlip2  25168  c1liplem1  25169  dvle  25180  dvivthlem1  25181  dvne0  25184  lhop1lem  25186  dvcnvrelem1  25190  dvfsumle  25194  dvfsumge  25195  dvfsumabs  25196  dvfsumlem2  25200  ftc1a  25210  ftc1lem4  25212  ftc1lem5  25213  ftc1lem6  25214  ftc1  25215  ftc2  25217  itgparts  25220  itgsubstlem  25221  itgsubst  25222  itgpowd  25223  reeff1olem  25614  efcvx  25617  cos0pilt1  25697  tanord1  25702  logccv  25827  loglesqrt  25920  chordthm  25996  amgmlem  26148  lgamgulmlem2  26188  eliccioo  31214  xrge0mulc1cn  31900  omssubadd  32276  ftc2re  32587  fdvposlt  32588  fdvneggt  32589  fdvposle  32590  fdvnegge  32591  circlemeth  32629  logdivsqrle  32639  ivthALT  34533  iccioo01  35507  itg2gt0cn  35841  ftc1cnnclem  35857  ftc1cnnc  35858  ftc2nc  35868  areacirc  35879  lcmineqlem10  40053  lcmineqlem12  40055  lhe4.4ex1a  41954  chordthmALT  42560  iccnct  43086  limciccioolb  43169  limcicciooub  43185  icccncfext  43435  cncfiooicclem1  43441  cncfioobdlem  43444  cncfioobd  43445  itgsin0pilem1  43498  iblioosinexp  43501  itgsinexplem1  43502  itgsinexp  43503  ditgeqiooicc  43508  itgcoscmulx  43517  ibliooicc  43519  itgsincmulx  43522  itgsubsticclem  43523  itgioocnicc  43525  iblcncfioo  43526  itgsbtaddcnst  43530  dirkeritg  43650  fourierdlem20  43675  fourierdlem38  43693  fourierdlem39  43694  fourierdlem46  43700  fourierdlem62  43716  fourierdlem68  43722  fourierdlem69  43723  fourierdlem70  43724  fourierdlem72  43726  fourierdlem73  43727  fourierdlem74  43728  fourierdlem75  43729  fourierdlem76  43730  fourierdlem80  43734  fourierdlem81  43735  fourierdlem82  43736  fourierdlem83  43737  fourierdlem84  43738  fourierdlem85  43739  fourierdlem88  43742  fourierdlem92  43746  fourierdlem93  43747  fourierdlem100  43754  fourierdlem101  43755  fourierdlem103  43757  fourierdlem104  43758  fourierdlem107  43761  fourierdlem111  43765  fourierdlem112  43766  sqwvfoura  43776  sqwvfourb  43777  etransclem18  43800  etransclem46  43828  hoicvrrex  44101  iooii  46222