Theorem ioossicc 13386

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

Syntax hints:   ⊆ wss 3889  (class class class)co 7367   < clt 11179   ≤ cle 11180  (,)cioo 13298  [,]cicc 13301

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 2708  ax-sep 5231  ax-nul 5241  ax-pow 5307  ax-pr 5375  ax-un 7689  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 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-mpt 5167  df-id 5526  df-po 5539  df-so 5540  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505  df-fv 6506  df-ov 7370  df-oprab 7371  df-mpo 7372  df-er 8643  df-en 8894  df-dom 8895  df-sdom 8896  df-pnf 11181  df-mnf 11182  df-xr 11183  df-ltxr 11184  df-le 11185  df-ioo 13302  df-icc 13305

This theorem is referenced by:  ioodisj  13435  iccntr  24787  ivth2  25422  ivthle  25423  ivthle2  25424  ovolioo  25535  uniiccvol  25547  itgioo  25783  rollelem  25956  rolle  25957  cmvth  25958  dvlip  25960  dvlipcn  25961  dvlip2  25962  c1liplem1  25963  dvle  25974  dvivthlem1  25975  dvne0  25978  lhop1lem  25980  dvcnvrelem1  25984  dvfsumle  25988  dvfsumge  25989  dvfsumabs  25990  dvfsumlem2  25994  ftc1a  26004  ftc1lem4  26006  ftc1lem5  26007  ftc1lem6  26008  ftc1  26009  ftc2  26011  itgparts  26014  itgsubstlem  26015  itgsubst  26016  itgpowd  26017  reeff1olem  26411  efcvx  26414  cos0pilt1  26496  tanord1  26501  logccv  26627  loglesqrt  26725  chordthm  26801  amgmlem  26953  lgamgulmlem2  26993  eliccioo  32990  xrge0mulc1cn  34085  omssubadd  34444  ftc2re  34742  fdvposlt  34743  fdvneggt  34744  fdvposle  34745  fdvnegge  34746  circlemeth  34784  logdivsqrle  34794  ivthALT  36517  iccioo01  37643  itg2gt0cn  37996  ftc1cnnclem  38012  ftc1cnnc  38013  ftc2nc  38023  areacirc  38034  lcmineqlem10  42477  lcmineqlem12  42479  lhe4.4ex1a  44756  chordthmALT  45359  iccnct  45971  limciccioolb  46051  limcicciooub  46065  icccncfext  46315  cncfiooicclem1  46321  cncfioobdlem  46324  cncfioobd  46325  itgsin0pilem1  46378  iblioosinexp  46381  itgsinexplem1  46382  itgsinexp  46383  ditgeqiooicc  46388  itgcoscmulx  46397  ibliooicc  46399  itgsincmulx  46402  itgsubsticclem  46403  itgioocnicc  46405  iblcncfioo  46406  itgsbtaddcnst  46410  dirkeritg  46530  fourierdlem20  46555  fourierdlem38  46573  fourierdlem39  46574  fourierdlem46  46580  fourierdlem62  46596  fourierdlem68  46602  fourierdlem69  46603  fourierdlem70  46604  fourierdlem72  46606  fourierdlem73  46607  fourierdlem74  46608  fourierdlem75  46609  fourierdlem76  46610  fourierdlem80  46614  fourierdlem81  46615  fourierdlem82  46616  fourierdlem83  46617  fourierdlem84  46618  fourierdlem85  46619  fourierdlem88  46622  fourierdlem92  46626  fourierdlem93  46627  fourierdlem100  46634  fourierdlem101  46635  fourierdlem103  46637  fourierdlem104  46638  fourierdlem107  46641  fourierdlem111  46645  fourierdlem112  46646  sqwvfoura  46656  sqwvfourb  46657  etransclem18  46680  etransclem46  46708  hoicvrrex  46984  iooii  49393