Theorem ioossicc 13361

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

Syntax hints:   ⊆ wss 3903  (class class class)co 7368   < clt 11178   ≤ cle 11179  (,)cioo 13273  [,]cicc 13276

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 5243  ax-nul 5253  ax-pow 5312  ax-pr 5379  ax-un 7690  ax-cnex 11094  ax-resscn 11095  ax-pre-lttri 11112  ax-pre-lttrn 11113

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 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-po 5540  df-so 5541  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-ov 7371  df-oprab 7372  df-mpo 7373  df-er 8645  df-en 8896  df-dom 8897  df-sdom 8898  df-pnf 11180  df-mnf 11181  df-xr 11182  df-ltxr 11183  df-le 11184  df-ioo 13277  df-icc 13280

This theorem is referenced by:  ioodisj  13410  iccntr  24778  ivth2  25424  ivthle  25425  ivthle2  25426  ovolioo  25537  uniiccvol  25549  itgioo  25785  rollelem  25961  rolle  25962  cmvth  25963  cmvthOLD  25964  dvlip  25966  dvlipcn  25967  dvlip2  25968  c1liplem1  25969  dvle  25980  dvivthlem1  25981  dvne0  25984  lhop1lem  25986  dvcnvrelem1  25990  dvfsumle  25994  dvfsumleOLD  25995  dvfsumge  25996  dvfsumabs  25997  dvfsumlem2  26001  dvfsumlem2OLD  26002  ftc1a  26012  ftc1lem4  26014  ftc1lem5  26015  ftc1lem6  26016  ftc1  26017  ftc2  26019  itgparts  26022  itgsubstlem  26023  itgsubst  26024  itgpowd  26025  reeff1olem  26424  efcvx  26427  cos0pilt1  26509  tanord1  26514  logccv  26640  loglesqrt  26739  chordthm  26815  amgmlem  26968  lgamgulmlem2  27008  eliccioo  33022  xrge0mulc1cn  34118  omssubadd  34477  ftc2re  34775  fdvposlt  34776  fdvneggt  34777  fdvposle  34778  fdvnegge  34779  circlemeth  34817  logdivsqrle  34827  ivthALT  36548  iccioo01  37576  itg2gt0cn  37920  ftc1cnnclem  37936  ftc1cnnc  37937  ftc2nc  37947  areacirc  37958  lcmineqlem10  42402  lcmineqlem12  42404  lhe4.4ex1a  44679  chordthmALT  45282  iccnct  45895  limciccioolb  45975  limcicciooub  45989  icccncfext  46239  cncfiooicclem1  46245  cncfioobdlem  46248  cncfioobd  46249  itgsin0pilem1  46302  iblioosinexp  46305  itgsinexplem1  46306  itgsinexp  46307  ditgeqiooicc  46312  itgcoscmulx  46321  ibliooicc  46323  itgsincmulx  46326  itgsubsticclem  46327  itgioocnicc  46329  iblcncfioo  46330  itgsbtaddcnst  46334  dirkeritg  46454  fourierdlem20  46479  fourierdlem38  46497  fourierdlem39  46498  fourierdlem46  46504  fourierdlem62  46520  fourierdlem68  46526  fourierdlem69  46527  fourierdlem70  46528  fourierdlem72  46530  fourierdlem73  46531  fourierdlem74  46532  fourierdlem75  46533  fourierdlem76  46534  fourierdlem80  46538  fourierdlem81  46539  fourierdlem82  46540  fourierdlem83  46541  fourierdlem84  46542  fourierdlem85  46543  fourierdlem88  46546  fourierdlem92  46550  fourierdlem93  46551  fourierdlem100  46558  fourierdlem101  46559  fourierdlem103  46561  fourierdlem104  46562  fourierdlem107  46565  fourierdlem111  46569  fourierdlem112  46570  sqwvfoura  46580  sqwvfourb  46581  etransclem18  46604  etransclem46  46632  hoicvrrex  46908  iooii  49271