Theorem ioossicc 13360

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

Syntax hints:   ⊆ wss 3913  (class class class)co 7362   < clt 11198   ≤ cle 11199  (,)cioo 13274  [,]cicc 13277

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677  ax-cnex 11116  ax-resscn 11117  ax-pre-lttri 11134  ax-pre-lttrn 11135

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rab 3406  df-v 3448  df-sbc 3743  df-csb 3859  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-opab 5173  df-mpt 5194  df-id 5536  df-po 5550  df-so 5551  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-ov 7365  df-oprab 7366  df-mpo 7367  df-er 8655  df-en 8891  df-dom 8892  df-sdom 8893  df-pnf 11200  df-mnf 11201  df-xr 11202  df-ltxr 11203  df-le 11204  df-ioo 13278  df-icc 13281

This theorem is referenced by:  ioodisj  13409  iccntr  24221  ivth2  24856  ivthle  24857  ivthle2  24858  ovolioo  24969  uniiccvol  24981  itgioo  25217  rollelem  25390  rolle  25391  cmvth  25392  dvlip  25394  dvlipcn  25395  dvlip2  25396  c1liplem1  25397  dvle  25408  dvivthlem1  25409  dvne0  25412  lhop1lem  25414  dvcnvrelem1  25418  dvfsumle  25422  dvfsumge  25423  dvfsumabs  25424  dvfsumlem2  25428  ftc1a  25438  ftc1lem4  25440  ftc1lem5  25441  ftc1lem6  25442  ftc1  25443  ftc2  25445  itgparts  25448  itgsubstlem  25449  itgsubst  25450  itgpowd  25451  reeff1olem  25842  efcvx  25845  cos0pilt1  25925  tanord1  25930  logccv  26055  loglesqrt  26148  chordthm  26224  amgmlem  26376  lgamgulmlem2  26416  eliccioo  31857  xrge0mulc1cn  32611  omssubadd  32989  ftc2re  33300  fdvposlt  33301  fdvneggt  33302  fdvposle  33303  fdvnegge  33304  circlemeth  33342  logdivsqrle  33352  ivthALT  34883  iccioo01  35871  itg2gt0cn  36206  ftc1cnnclem  36222  ftc1cnnc  36223  ftc2nc  36233  areacirc  36244  lcmineqlem10  40568  lcmineqlem12  40570  lhe4.4ex1a  42731  chordthmALT  43337  iccnct  43899  limciccioolb  43982  limcicciooub  43998  icccncfext  44248  cncfiooicclem1  44254  cncfioobdlem  44257  cncfioobd  44258  itgsin0pilem1  44311  iblioosinexp  44314  itgsinexplem1  44315  itgsinexp  44316  ditgeqiooicc  44321  itgcoscmulx  44330  ibliooicc  44332  itgsincmulx  44335  itgsubsticclem  44336  itgioocnicc  44338  iblcncfioo  44339  itgsbtaddcnst  44343  dirkeritg  44463  fourierdlem20  44488  fourierdlem38  44506  fourierdlem39  44507  fourierdlem46  44513  fourierdlem62  44529  fourierdlem68  44535  fourierdlem69  44536  fourierdlem70  44537  fourierdlem72  44539  fourierdlem73  44540  fourierdlem74  44541  fourierdlem75  44542  fourierdlem76  44543  fourierdlem80  44547  fourierdlem81  44548  fourierdlem82  44549  fourierdlem83  44550  fourierdlem84  44551  fourierdlem85  44552  fourierdlem88  44555  fourierdlem92  44559  fourierdlem93  44560  fourierdlem100  44567  fourierdlem101  44568  fourierdlem103  44570  fourierdlem104  44571  fourierdlem107  44574  fourierdlem111  44578  fourierdlem112  44579  sqwvfoura  44589  sqwvfourb  44590  etransclem18  44613  etransclem46  44641  hoicvrrex  44917  iooii  47070