Theorem ioossicc 13545

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

This proof depends on syntax axioms:   ⊆ wss 3899  (class class class)co 7412   < clt 11324   ≤ cle 11325  (,)cioo 13457  [,]cicc 13460

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7740  ax-cnex 11237  ax-resscn 11238  ax-pre-lttri 11255  ax-pre-lttrn 11256

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3063  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5546  df-po 5559  df-so 5560  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6487  df-fun 6533  df-fn 6534  df-f 6535  df-f1 6536  df-fo 6537  df-f1o 6538  df-fv 6539  df-ov 7415  df-oprab 7416  df-mpo 7417  df-er 8701  df-en 8958  df-dom 8959  df-sdom 8960  df-pnf 11326  df-mnf 11327  df-xr 11328  df-ltxr 11329  df-le 11330  df-ioo 13461  df-icc 13464

This theorem is used by:  ioodisj  13594  iccntr  25121  ivth2  25756  ivthle  25757  ivthle2  25758  ovolioo  25869  uniiccvol  25881  itgioo  26116  rollelem  26289  rolle  26290  cmvth  26291  dvlip  26293  dvlipcn  26294  dvlip2  26295  c1liplem1  26296  dvle  26307  dvivthlem1  26308  dvne0  26311  lhop1lem  26313  dvcnvrelem1  26317  dvfsumle  26321  dvfsumge  26322  dvfsumabs  26323  dvfsumlem2  26327  ftc1a  26337  ftc1lem4  26339  ftc1lem5  26340  ftc1lem6  26341  ftc1  26342  ftc2  26344  itgparts  26347  itgsubstlem  26348  itgsubst  26349  itgpowd  26350  reeff1olem  26755  efcvx  26758  cos0pilt1  26842  tanord1  26847  logccv  26973  loglesqrt  27071  chordthm  27147  amgmlem  27299  lgamgulmlem2  27339  eliccioo  33479  xrge0mulc1cn  34555  omssubadd  34915  ftc2re  35210  fdvposlt  35211  fdvneggt  35212  fdvposle  35213  fdvnegge  35214  circlemeth  35252  logdivsqrle  35262  ivthALT  37093  iccioo01  38218  itg2gt0cn  38561  ftc1cnnclem  38577  ftc1cnnc  38578  ftc2nc  38588  areacirc  38599  lcmineqlem10  43056  lcmineqlem12  43058  lhe4.4ex1a  45272  chordthmALT  45874  iccnct  46497  limciccioolb  46577  limcicciooub  46591  icccncfext  46841  cncfiooicclem1  46847  cncfioobdlem  46850  cncfioobd  46851  itgsin0pilem1  46904  iblioosinexp  46907  itgsinexplem1  46908  itgsinexp  46909  ditgeqiooicc  46914  itgcoscmulx  46923  ibliooicc  46925  itgsincmulx  46928  itgsubsticclem  46929  itgioocnicc  46931  iblcncfioo  46932  itgsbtaddcnst  46936  dirkeritg  47056  fourierdlem20  47081  fourierdlem38  47099  fourierdlem39  47100  fourierdlem46  47106  fourierdlem62  47122  fourierdlem68  47128  fourierdlem69  47129  fourierdlem70  47130  fourierdlem72  47132  fourierdlem73  47133  fourierdlem74  47134  fourierdlem75  47135  fourierdlem76  47136  fourierdlem80  47140  fourierdlem81  47141  fourierdlem82  47142  fourierdlem83  47143  fourierdlem84  47144  fourierdlem85  47145  fourierdlem88  47148  fourierdlem92  47152  fourierdlem93  47153  fourierdlem100  47160  fourierdlem101  47161  fourierdlem103  47163  fourierdlem104  47164  fourierdlem107  47167  fourierdlem111  47171  fourierdlem112  47172  sqwvfoura  47182  sqwvfourb  47183  etransclem18  47206  etransclem46  47234  hoicvrrex  47510  iooii  49970