Theorem iccssred 13592

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 13587	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ)
4	1, 2, 3	syl2anc 596	1 ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147   ⊆ wss 3900  (class class class)co 7443  ℝcr 11226  [,]cicc 13506

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5252  ax-nul 5263  ax-pow 5331  ax-pr 5395  ax-un 7775  ax-cnex 11283  ax-resscn 11284  ax-pre-lttri 11301  ax-pre-lttrn 11302

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 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3066  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5171  df-mpt 5190  df-id 5550  df-po 5563  df-so 5564  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6512  df-fun 6560  df-fn 6561  df-f 6562  df-f1 6563  df-fo 6564  df-f1o 6565  df-fv 6566  df-ov 7446  df-oprab 7447  df-mpo 7448  df-er 8745  df-en 9002  df-dom 9003  df-sdom 9004  df-pnf 11372  df-mnf 11373  df-xr 11374  df-ltxr 11375  df-le 11376  df-icc 13510

This theorem is used by:  dvmptresicc  26266  cmvth  26341  dvfsumle  26371  iccshift  46735  eliccelioc  46738  limciccioolb  46838  limcicciooub  46852  icccncfext  47102  cncfiooicclem1  47108  itgcoscmulx  47184  ibliooicc  47186  itgsincmulx  47189  itgsubsticclem  47190  itgiccshift  47195  itgperiod  47196  itgsbtaddcnst  47197  dirkeritg  47317  fourierdlem20  47342  fourierdlem25  47347  fourierdlem39  47361  fourierdlem40  47362  fourierdlem42  47364  fourierdlem46  47367  fourierdlem50  47371  fourierdlem51  47372  fourierdlem52  47373  fourierdlem54  47375  fourierdlem58  47379  fourierdlem64  47385  fourierdlem68  47389  fourierdlem73  47394  fourierdlem74  47395  fourierdlem75  47396  fourierdlem76  47397  fourierdlem78  47399  fourierdlem79  47400  fourierdlem80  47401  fourierdlem81  47402  fourierdlem84  47405  fourierdlem88  47409  fourierdlem89  47410  fourierdlem90  47411  fourierdlem91  47412  fourierdlem100  47421  fourierdlem103  47424  fourierdlem104  47425  fourierdlem107  47428  fourierdlem111  47432  fourierdlem112  47433  etransclem18  47467  etransclem46  47495  rrxsnicc  47515  hoidmv1lelem1  47806  hoidmv1lelem3  47808  hoidmvlelem1  47810  hoidmvlelem2  47811  hoidmvlelem4  47813