Theorem ioossicc 13493

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

Syntax hints:   ⊆ wss 3976  (class class class)co 7448   < clt 11324   ≤ cle 11325  (,)cioo 13407  [,]cicc 13410

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770  ax-cnex 11240  ax-resscn 11241  ax-pre-lttri 11258  ax-pre-lttrn 11259

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-nel 3053  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-mpt 5250  df-id 5593  df-po 5607  df-so 5608  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-ov 7451  df-oprab 7452  df-mpo 7453  df-er 8763  df-en 9004  df-dom 9005  df-sdom 9006  df-pnf 11326  df-mnf 11327  df-xr 11328  df-ltxr 11329  df-le 11330  df-ioo 13411  df-icc 13414

This theorem is referenced by:  ioodisj  13542  iccntr  24862  ivth2  25509  ivthle  25510  ivthle2  25511  ovolioo  25622  uniiccvol  25634  itgioo  25871  rollelem  26047  rolle  26048  cmvth  26049  cmvthOLD  26050  dvlip  26052  dvlipcn  26053  dvlip2  26054  c1liplem1  26055  dvle  26066  dvivthlem1  26067  dvne0  26070  lhop1lem  26072  dvcnvrelem1  26076  dvfsumle  26080  dvfsumleOLD  26081  dvfsumge  26082  dvfsumabs  26083  dvfsumlem2  26087  dvfsumlem2OLD  26088  ftc1a  26098  ftc1lem4  26100  ftc1lem5  26101  ftc1lem6  26102  ftc1  26103  ftc2  26105  itgparts  26108  itgsubstlem  26109  itgsubst  26110  itgpowd  26111  reeff1olem  26508  efcvx  26511  cos0pilt1  26592  tanord1  26597  logccv  26723  loglesqrt  26822  chordthm  26898  amgmlem  27051  lgamgulmlem2  27091  eliccioo  32895  xrge0mulc1cn  33887  omssubadd  34265  ftc2re  34575  fdvposlt  34576  fdvneggt  34577  fdvposle  34578  fdvnegge  34579  circlemeth  34617  logdivsqrle  34627  ivthALT  36301  iccioo01  37293  itg2gt0cn  37635  ftc1cnnclem  37651  ftc1cnnc  37652  ftc2nc  37662  areacirc  37673  lcmineqlem10  41995  lcmineqlem12  41997  lhe4.4ex1a  44298  chordthmALT  44904  iccnct  45459  limciccioolb  45542  limcicciooub  45558  icccncfext  45808  cncfiooicclem1  45814  cncfioobdlem  45817  cncfioobd  45818  itgsin0pilem1  45871  iblioosinexp  45874  itgsinexplem1  45875  itgsinexp  45876  ditgeqiooicc  45881  itgcoscmulx  45890  ibliooicc  45892  itgsincmulx  45895  itgsubsticclem  45896  itgioocnicc  45898  iblcncfioo  45899  itgsbtaddcnst  45903  dirkeritg  46023  fourierdlem20  46048  fourierdlem38  46066  fourierdlem39  46067  fourierdlem46  46073  fourierdlem62  46089  fourierdlem68  46095  fourierdlem69  46096  fourierdlem70  46097  fourierdlem72  46099  fourierdlem73  46100  fourierdlem74  46101  fourierdlem75  46102  fourierdlem76  46103  fourierdlem80  46107  fourierdlem81  46108  fourierdlem82  46109  fourierdlem83  46110  fourierdlem84  46111  fourierdlem85  46112  fourierdlem88  46115  fourierdlem92  46119  fourierdlem93  46120  fourierdlem100  46127  fourierdlem101  46128  fourierdlem103  46130  fourierdlem104  46131  fourierdlem107  46134  fourierdlem111  46138  fourierdlem112  46139  sqwvfoura  46149  sqwvfourb  46150  etransclem18  46173  etransclem46  46201  hoicvrrex  46477  iooii  48597