Theorem iccssred 13401

Description: A closed real interval is a set of reals. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

Hypotheses

Ref	Expression
iccssred.1	⊢ (𝜑 → 𝐴 ∈ ℝ)
iccssred.2	⊢ (𝜑 → 𝐵 ∈ ℝ)

Assertion

Ref	Expression
iccssred	⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)

Proof of Theorem iccssred

Step	Hyp	Ref	Expression
1		iccssred.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ)
2		iccssred.2	. 2 ⊢ (𝜑 → 𝐵 ∈ ℝ)
3		iccssre 13396	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ)
4	1, 2, 3	syl2anc 584	1 ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2109   ⊆ wss 3916  (class class class)co 7389  ℝcr 11073  [,]cicc 13315

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5253  ax-nul 5263  ax-pow 5322  ax-pr 5389  ax-un 7713  ax-cnex 11130  ax-resscn 11131  ax-pre-lttri 11148  ax-pre-lttrn 11149

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-nel 3031  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-sbc 3756  df-csb 3865  df-dif 3919  df-un 3921  df-in 3923  df-ss 3933  df-nul 4299  df-if 4491  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-br 5110  df-opab 5172  df-mpt 5191  df-id 5535  df-po 5548  df-so 5549  df-xp 5646  df-rel 5647  df-cnv 5648  df-co 5649  df-dm 5650  df-rn 5651  df-res 5652  df-ima 5653  df-iota 6466  df-fun 6515  df-fn 6516  df-f 6517  df-f1 6518  df-fo 6519  df-f1o 6520  df-fv 6521  df-ov 7392  df-oprab 7393  df-mpo 7394  df-er 8673  df-en 8921  df-dom 8922  df-sdom 8923  df-pnf 11216  df-mnf 11217  df-xr 11218  df-ltxr 11219  df-le 11220  df-icc 13319

This theorem is referenced by:  dvmptresicc  25823  cmvth  25901  dvfsumle  25932  iccshift  45509  eliccelioc  45512  limciccioolb  45612  limcicciooub  45628  icccncfext  45878  cncfiooicclem1  45884  itgcoscmulx  45960  ibliooicc  45962  itgsincmulx  45965  itgsubsticclem  45966  itgiccshift  45971  itgperiod  45972  itgsbtaddcnst  45973  dirkeritg  46093  fourierdlem20  46118  fourierdlem25  46123  fourierdlem39  46137  fourierdlem40  46138  fourierdlem42  46140  fourierdlem46  46143  fourierdlem50  46147  fourierdlem51  46148  fourierdlem52  46149  fourierdlem54  46151  fourierdlem58  46155  fourierdlem64  46161  fourierdlem68  46165  fourierdlem73  46170  fourierdlem74  46171  fourierdlem75  46172  fourierdlem76  46173  fourierdlem78  46175  fourierdlem79  46176  fourierdlem80  46177  fourierdlem81  46178  fourierdlem84  46181  fourierdlem88  46185  fourierdlem89  46186  fourierdlem90  46187  fourierdlem91  46188  fourierdlem100  46197  fourierdlem103  46200  fourierdlem104  46201  fourierdlem107  46204  fourierdlem111  46208  fourierdlem112  46209  etransclem18  46243  etransclem46  46271  rrxsnicc  46291  hoidmv1lelem1  46582  hoidmv1lelem3  46584  hoidmvlelem1  46586  hoidmvlelem2  46587  hoidmvlelem4  46589