Theorem ioossicc 13448

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

Syntax hints:   ⊆ wss 3926  (class class class)co 7403   < clt 11267   ≤ cle 11268  (,)cioo 13360  [,]cicc 13363

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pow 5335  ax-pr 5402  ax-un 7727  ax-cnex 11183  ax-resscn 11184  ax-pre-lttri 11201  ax-pre-lttrn 11202

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-sbc 3766  df-csb 3875  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-mpt 5202  df-id 5548  df-po 5561  df-so 5562  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-iota 6483  df-fun 6532  df-fn 6533  df-f 6534  df-f1 6535  df-fo 6536  df-f1o 6537  df-fv 6538  df-ov 7406  df-oprab 7407  df-mpo 7408  df-er 8717  df-en 8958  df-dom 8959  df-sdom 8960  df-pnf 11269  df-mnf 11270  df-xr 11271  df-ltxr 11272  df-le 11273  df-ioo 13364  df-icc 13367

This theorem is referenced by:  ioodisj  13497  iccntr  24759  ivth2  25406  ivthle  25407  ivthle2  25408  ovolioo  25519  uniiccvol  25531  itgioo  25767  rollelem  25943  rolle  25944  cmvth  25945  cmvthOLD  25946  dvlip  25948  dvlipcn  25949  dvlip2  25950  c1liplem1  25951  dvle  25962  dvivthlem1  25963  dvne0  25966  lhop1lem  25968  dvcnvrelem1  25972  dvfsumle  25976  dvfsumleOLD  25977  dvfsumge  25978  dvfsumabs  25979  dvfsumlem2  25983  dvfsumlem2OLD  25984  ftc1a  25994  ftc1lem4  25996  ftc1lem5  25997  ftc1lem6  25998  ftc1  25999  ftc2  26001  itgparts  26004  itgsubstlem  26005  itgsubst  26006  itgpowd  26007  reeff1olem  26406  efcvx  26409  cos0pilt1  26491  tanord1  26496  logccv  26622  loglesqrt  26721  chordthm  26797  amgmlem  26950  lgamgulmlem2  26990  eliccioo  32851  xrge0mulc1cn  33918  omssubadd  34278  ftc2re  34576  fdvposlt  34577  fdvneggt  34578  fdvposle  34579  fdvnegge  34580  circlemeth  34618  logdivsqrle  34628  ivthALT  36299  iccioo01  37291  itg2gt0cn  37645  ftc1cnnclem  37661  ftc1cnnc  37662  ftc2nc  37672  areacirc  37683  lcmineqlem10  41997  lcmineqlem12  41999  lhe4.4ex1a  44301  chordthmALT  44905  iccnct  45518  limciccioolb  45598  limcicciooub  45614  icccncfext  45864  cncfiooicclem1  45870  cncfioobdlem  45873  cncfioobd  45874  itgsin0pilem1  45927  iblioosinexp  45930  itgsinexplem1  45931  itgsinexp  45932  ditgeqiooicc  45937  itgcoscmulx  45946  ibliooicc  45948  itgsincmulx  45951  itgsubsticclem  45952  itgioocnicc  45954  iblcncfioo  45955  itgsbtaddcnst  45959  dirkeritg  46079  fourierdlem20  46104  fourierdlem38  46122  fourierdlem39  46123  fourierdlem46  46129  fourierdlem62  46145  fourierdlem68  46151  fourierdlem69  46152  fourierdlem70  46153  fourierdlem72  46155  fourierdlem73  46156  fourierdlem74  46157  fourierdlem75  46158  fourierdlem76  46159  fourierdlem80  46163  fourierdlem81  46164  fourierdlem82  46165  fourierdlem83  46166  fourierdlem84  46167  fourierdlem85  46168  fourierdlem88  46171  fourierdlem92  46175  fourierdlem93  46176  fourierdlem100  46183  fourierdlem101  46184  fourierdlem103  46186  fourierdlem104  46187  fourierdlem107  46190  fourierdlem111  46194  fourierdlem112  46195  sqwvfoura  46205  sqwvfourb  46206  etransclem18  46229  etransclem46  46257  hoicvrrex  46533  iooii  48840