Theorem ioossicc 13445

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

Syntax hints:   ⊆ wss 3944  (class class class)co 7419   < clt 11280   ≤ cle 11281  (,)cioo 13359  [,]cicc 13362

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-sep 5300  ax-nul 5307  ax-pow 5365  ax-pr 5429  ax-un 7741  ax-cnex 11196  ax-resscn 11197  ax-pre-lttri 11214  ax-pre-lttrn 11215

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2930  df-nel 3036  df-ral 3051  df-rex 3060  df-rab 3419  df-v 3463  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4323  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4910  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5576  df-po 5590  df-so 5591  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-iota 6501  df-fun 6551  df-fn 6552  df-f 6553  df-f1 6554  df-fo 6555  df-f1o 6556  df-fv 6557  df-ov 7422  df-oprab 7423  df-mpo 7424  df-er 8725  df-en 8965  df-dom 8966  df-sdom 8967  df-pnf 11282  df-mnf 11283  df-xr 11284  df-ltxr 11285  df-le 11286  df-ioo 13363  df-icc 13366

This theorem is referenced by:  ioodisj  13494  iccntr  24781  ivth2  25428  ivthle  25429  ivthle2  25430  ovolioo  25541  uniiccvol  25553  itgioo  25789  rollelem  25965  rolle  25966  cmvth  25967  cmvthOLD  25968  dvlip  25970  dvlipcn  25971  dvlip2  25972  c1liplem1  25973  dvle  25984  dvivthlem1  25985  dvne0  25988  lhop1lem  25990  dvcnvrelem1  25994  dvfsumle  25998  dvfsumleOLD  25999  dvfsumge  26000  dvfsumabs  26001  dvfsumlem2  26005  dvfsumlem2OLD  26006  ftc1a  26016  ftc1lem4  26018  ftc1lem5  26019  ftc1lem6  26020  ftc1  26021  ftc2  26023  itgparts  26026  itgsubstlem  26027  itgsubst  26028  itgpowd  26029  reeff1olem  26428  efcvx  26431  cos0pilt1  26511  tanord1  26516  logccv  26642  loglesqrt  26738  chordthm  26814  amgmlem  26967  lgamgulmlem2  27007  eliccioo  32739  xrge0mulc1cn  33673  omssubadd  34051  ftc2re  34361  fdvposlt  34362  fdvneggt  34363  fdvposle  34364  fdvnegge  34365  circlemeth  34403  logdivsqrle  34413  ivthALT  35950  iccioo01  36937  itg2gt0cn  37279  ftc1cnnclem  37295  ftc1cnnc  37296  ftc2nc  37306  areacirc  37317  lcmineqlem10  41641  lcmineqlem12  41643  lhe4.4ex1a  43908  chordthmALT  44514  iccnct  45064  limciccioolb  45147  limcicciooub  45163  icccncfext  45413  cncfiooicclem1  45419  cncfioobdlem  45422  cncfioobd  45423  itgsin0pilem1  45476  iblioosinexp  45479  itgsinexplem1  45480  itgsinexp  45481  ditgeqiooicc  45486  itgcoscmulx  45495  ibliooicc  45497  itgsincmulx  45500  itgsubsticclem  45501  itgioocnicc  45503  iblcncfioo  45504  itgsbtaddcnst  45508  dirkeritg  45628  fourierdlem20  45653  fourierdlem38  45671  fourierdlem39  45672  fourierdlem46  45678  fourierdlem62  45694  fourierdlem68  45700  fourierdlem69  45701  fourierdlem70  45702  fourierdlem72  45704  fourierdlem73  45705  fourierdlem74  45706  fourierdlem75  45707  fourierdlem76  45708  fourierdlem80  45712  fourierdlem81  45713  fourierdlem82  45714  fourierdlem83  45715  fourierdlem84  45716  fourierdlem85  45717  fourierdlem88  45720  fourierdlem92  45724  fourierdlem93  45725  fourierdlem100  45732  fourierdlem101  45733  fourierdlem103  45735  fourierdlem104  45736  fourierdlem107  45739  fourierdlem111  45743  fourierdlem112  45744  sqwvfoura  45754  sqwvfourb  45755  etransclem18  45778  etransclem46  45806  hoicvrrex  46082  iooii  48122