Theorem ioossicc 12571

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

Syntax hints:   ⊆ wss 3792  (class class class)co 6922   < clt 10411   ≤ cle 10412  (,)cioo 12487  [,]cicc 12490

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-sep 5017  ax-nul 5025  ax-pow 5077  ax-pr 5138  ax-un 7226  ax-cnex 10328  ax-resscn 10329  ax-pre-lttri 10346  ax-pre-lttrn 10347

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ne 2970  df-nel 3076  df-ral 3095  df-rex 3096  df-rab 3099  df-v 3400  df-sbc 3653  df-csb 3752  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-nul 4142  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-op 4405  df-uni 4672  df-br 4887  df-opab 4949  df-mpt 4966  df-id 5261  df-po 5274  df-so 5275  df-xp 5361  df-rel 5362  df-cnv 5363  df-co 5364  df-dm 5365  df-rn 5366  df-res 5367  df-ima 5368  df-iota 6099  df-fun 6137  df-fn 6138  df-f 6139  df-f1 6140  df-fo 6141  df-f1o 6142  df-fv 6143  df-ov 6925  df-oprab 6926  df-mpt2 6927  df-er 8026  df-en 8242  df-dom 8243  df-sdom 8244  df-pnf 10413  df-mnf 10414  df-xr 10415  df-ltxr 10416  df-le 10417  df-ioo 12491  df-icc 12494

This theorem is referenced by:  ioodisj  12619  iccntr  23032  ivth2  23659  ivthle  23660  ivthle2  23661  ovolioo  23772  uniiccvol  23784  itgioo  24019  rollelem  24189  rolle  24190  cmvth  24191  dvlip  24193  dvlipcn  24194  dvlip2  24195  c1liplem1  24196  dvle  24207  dvivthlem1  24208  dvne0  24211  lhop1lem  24213  dvcnvrelem1  24217  dvfsumle  24221  dvfsumge  24222  dvfsumabs  24223  dvfsumlem2  24227  ftc1a  24237  ftc1lem4  24239  ftc1lem5  24240  ftc1lem6  24241  ftc1  24242  ftc2  24244  itgparts  24247  itgsubstlem  24248  itgsubst  24249  reeff1olem  24637  efcvx  24640  tanord1  24721  logccv  24846  loglesqrt  24939  chordthm  25015  amgmlem  25168  lgamgulmlem2  25208  eliccioo  30201  xrge0mulc1cn  30585  omssubadd  30960  ftc2re  31278  fdvposlt  31279  fdvneggt  31280  fdvposle  31281  fdvnegge  31282  circlemeth  31320  logdivsqrle  31330  ivthALT  32918  itg2gt0cn  34090  ftc1cnnclem  34108  ftc1cnnc  34109  ftc2nc  34119  areacirc  34130  itgpowd  38758  lhe4.4ex1a  39484  chordthmALT  40102  iccnct  40676  limciccioolb  40761  limcicciooub  40777  icccncfext  41028  cncfiooicclem1  41034  cncfioobdlem  41037  cncfioobd  41038  itgsin0pilem1  41093  iblioosinexp  41096  itgsinexplem1  41097  itgsinexp  41098  ditgeqiooicc  41103  itgcoscmulx  41112  ibliooicc  41114  itgsincmulx  41117  itgsubsticclem  41118  itgioocnicc  41120  iblcncfioo  41121  itgsbtaddcnst  41125  dirkeritg  41246  fourierdlem20  41271  fourierdlem38  41289  fourierdlem39  41290  fourierdlem46  41296  fourierdlem62  41312  fourierdlem68  41318  fourierdlem69  41319  fourierdlem70  41320  fourierdlem72  41322  fourierdlem73  41323  fourierdlem74  41324  fourierdlem75  41325  fourierdlem76  41326  fourierdlem80  41330  fourierdlem81  41331  fourierdlem82  41332  fourierdlem83  41333  fourierdlem84  41334  fourierdlem85  41335  fourierdlem88  41338  fourierdlem92  41342  fourierdlem93  41343  fourierdlem100  41350  fourierdlem101  41351  fourierdlem103  41353  fourierdlem104  41354  fourierdlem107  41357  fourierdlem111  41361  fourierdlem112  41362  sqwvfoura  41372  sqwvfourb  41373  etransclem18  41396  etransclem46  41424  hoicvrrex  41697