Theorem ioossicc 13490

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

This proof depends on syntax axioms:   ⊆ wss 3902  (class class class)co 7417   < clt 11271   ≤ cle 11272  (,)cioo 13402  [,]cicc 13405

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 2215  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pow 5334  ax-pr 5402  ax-un 7740  ax-cnex 11184  ax-resscn 11185  ax-pre-lttri 11202  ax-pre-lttrn 11203

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 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-nel 3064  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-mpt 5191  df-id 5554  df-po 5567  df-so 5568  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-ov 7420  df-oprab 7421  df-mpo 7422  df-er 8700  df-en 8957  df-dom 8958  df-sdom 8959  df-pnf 11273  df-mnf 11274  df-xr 11275  df-ltxr 11276  df-le 11277  df-ioo 13406  df-icc 13409

This theorem is used by:  ioodisj  13539  iccntr  25054  ivth2  25689  ivthle  25690  ivthle2  25691  ovolioo  25802  uniiccvol  25814  itgioo  26050  rollelem  26223  rolle  26224  cmvth  26225  dvlip  26227  dvlipcn  26228  dvlip2  26229  c1liplem1  26230  dvle  26241  dvivthlem1  26242  dvne0  26245  lhop1lem  26247  dvcnvrelem1  26251  dvfsumle  26255  dvfsumge  26256  dvfsumabs  26257  dvfsumlem2  26261  ftc1a  26271  ftc1lem4  26273  ftc1lem5  26274  ftc1lem6  26275  ftc1  26276  ftc2  26278  itgparts  26281  itgsubstlem  26282  itgsubst  26283  itgpowd  26284  reeff1olem  26689  efcvx  26692  cos0pilt1  26777  tanord1  26782  logccv  26908  loglesqrt  27006  chordthm  27082  amgmlem  27234  lgamgulmlem2  27274  eliccioo  33384  xrge0mulc1cn  34459  omssubadd  34819  ftc2re  35114  fdvposlt  35115  fdvneggt  35116  fdvposle  35117  fdvnegge  35118  circlemeth  35156  logdivsqrle  35166  ivthALT  36962  iccioo01  38089  itg2gt0cn  38432  ftc1cnnclem  38448  ftc1cnnc  38449  ftc2nc  38459  areacirc  38470  lcmineqlem10  42912  lcmineqlem12  42914  lhe4.4ex1a  45161  chordthmALT  45763  iccnct  46379  limciccioolb  46459  limcicciooub  46473  icccncfext  46723  cncfiooicclem1  46729  cncfioobdlem  46732  cncfioobd  46733  itgsin0pilem1  46786  iblioosinexp  46789  itgsinexplem1  46790  itgsinexp  46791  ditgeqiooicc  46796  itgcoscmulx  46805  ibliooicc  46807  itgsincmulx  46810  itgsubsticclem  46811  itgioocnicc  46813  iblcncfioo  46814  itgsbtaddcnst  46818  dirkeritg  46938  fourierdlem20  46963  fourierdlem38  46981  fourierdlem39  46982  fourierdlem46  46988  fourierdlem62  47004  fourierdlem68  47010  fourierdlem69  47011  fourierdlem70  47012  fourierdlem72  47014  fourierdlem73  47015  fourierdlem74  47016  fourierdlem75  47017  fourierdlem76  47018  fourierdlem80  47022  fourierdlem81  47023  fourierdlem82  47024  fourierdlem83  47025  fourierdlem84  47026  fourierdlem85  47027  fourierdlem88  47030  fourierdlem92  47034  fourierdlem93  47035  fourierdlem100  47042  fourierdlem101  47043  fourierdlem103  47045  fourierdlem104  47046  fourierdlem107  47049  fourierdlem111  47053  fourierdlem112  47054  sqwvfoura  47064  sqwvfourb  47065  etransclem18  47088  etransclem46  47116  hoicvrrex  47392  iooii  49852