Theorem ioossicc 13335

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

Syntax hints:   ⊆ wss 3898  (class class class)co 7352   < clt 11153   ≤ cle 11154  (,)cioo 13247  [,]cicc 13250

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-sep 5236  ax-nul 5246  ax-pow 5305  ax-pr 5372  ax-un 7674  ax-cnex 11069  ax-resscn 11070  ax-pre-lttri 11087  ax-pre-lttrn 11088

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ne 2930  df-nel 3034  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-sbc 3738  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4475  df-pw 4551  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-br 5094  df-opab 5156  df-mpt 5175  df-id 5514  df-po 5527  df-so 5528  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-fv 6494  df-ov 7355  df-oprab 7356  df-mpo 7357  df-er 8628  df-en 8876  df-dom 8877  df-sdom 8878  df-pnf 11155  df-mnf 11156  df-xr 11157  df-ltxr 11158  df-le 11159  df-ioo 13251  df-icc 13254

This theorem is referenced by:  ioodisj  13384  iccntr  24738  ivth2  25384  ivthle  25385  ivthle2  25386  ovolioo  25497  uniiccvol  25509  itgioo  25745  rollelem  25921  rolle  25922  cmvth  25923  cmvthOLD  25924  dvlip  25926  dvlipcn  25927  dvlip2  25928  c1liplem1  25929  dvle  25940  dvivthlem1  25941  dvne0  25944  lhop1lem  25946  dvcnvrelem1  25950  dvfsumle  25954  dvfsumleOLD  25955  dvfsumge  25956  dvfsumabs  25957  dvfsumlem2  25961  dvfsumlem2OLD  25962  ftc1a  25972  ftc1lem4  25974  ftc1lem5  25975  ftc1lem6  25976  ftc1  25977  ftc2  25979  itgparts  25982  itgsubstlem  25983  itgsubst  25984  itgpowd  25985  reeff1olem  26384  efcvx  26387  cos0pilt1  26469  tanord1  26474  logccv  26600  loglesqrt  26699  chordthm  26775  amgmlem  26928  lgamgulmlem2  26968  eliccioo  32918  xrge0mulc1cn  33975  omssubadd  34334  ftc2re  34632  fdvposlt  34633  fdvneggt  34634  fdvposle  34635  fdvnegge  34636  circlemeth  34674  logdivsqrle  34684  ivthALT  36400  iccioo01  37392  itg2gt0cn  37735  ftc1cnnclem  37751  ftc1cnnc  37752  ftc2nc  37762  areacirc  37773  lcmineqlem10  42151  lcmineqlem12  42153  lhe4.4ex1a  44446  chordthmALT  45049  iccnct  45665  limciccioolb  45745  limcicciooub  45759  icccncfext  46009  cncfiooicclem1  46015  cncfioobdlem  46018  cncfioobd  46019  itgsin0pilem1  46072  iblioosinexp  46075  itgsinexplem1  46076  itgsinexp  46077  ditgeqiooicc  46082  itgcoscmulx  46091  ibliooicc  46093  itgsincmulx  46096  itgsubsticclem  46097  itgioocnicc  46099  iblcncfioo  46100  itgsbtaddcnst  46104  dirkeritg  46224  fourierdlem20  46249  fourierdlem38  46267  fourierdlem39  46268  fourierdlem46  46274  fourierdlem62  46290  fourierdlem68  46296  fourierdlem69  46297  fourierdlem70  46298  fourierdlem72  46300  fourierdlem73  46301  fourierdlem74  46302  fourierdlem75  46303  fourierdlem76  46304  fourierdlem80  46308  fourierdlem81  46309  fourierdlem82  46310  fourierdlem83  46311  fourierdlem84  46312  fourierdlem85  46313  fourierdlem88  46316  fourierdlem92  46320  fourierdlem93  46321  fourierdlem100  46328  fourierdlem101  46329  fourierdlem103  46331  fourierdlem104  46332  fourierdlem107  46335  fourierdlem111  46339  fourierdlem112  46340  sqwvfoura  46350  sqwvfourb  46351  etransclem18  46374  etransclem46  46402  hoicvrrex  46678  iooii  49042