Theorem iccssred 13535

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   ⊆ wss 3898  (class class class)co 7408  ℝcr 11171  [,]cicc 13449

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 2213  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7734  ax-cnex 11228  ax-resscn 11229  ax-pre-lttri 11246  ax-pre-lttrn 11247

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 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5542  df-po 5555  df-so 5556  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660  df-iota 6483  df-fun 6529  df-fn 6530  df-f 6531  df-f1 6532  df-fo 6533  df-f1o 6534  df-fv 6535  df-ov 7411  df-oprab 7412  df-mpo 7413  df-er 8695  df-en 8952  df-dom 8953  df-sdom 8954  df-pnf 11317  df-mnf 11318  df-xr 11319  df-ltxr 11320  df-le 11321  df-icc 13453

This theorem is used by:  dvmptresicc  26198  cmvth  26273  dvfsumle  26303  iccshift  46452  eliccelioc  46455  limciccioolb  46555  limcicciooub  46569  icccncfext  46819  cncfiooicclem1  46825  itgcoscmulx  46901  ibliooicc  46903  itgsincmulx  46906  itgsubsticclem  46907  itgiccshift  46912  itgperiod  46913  itgsbtaddcnst  46914  dirkeritg  47034  fourierdlem20  47059  fourierdlem25  47064  fourierdlem39  47078  fourierdlem40  47079  fourierdlem42  47081  fourierdlem46  47084  fourierdlem50  47088  fourierdlem51  47089  fourierdlem52  47090  fourierdlem54  47092  fourierdlem58  47096  fourierdlem64  47102  fourierdlem68  47106  fourierdlem73  47111  fourierdlem74  47112  fourierdlem75  47113  fourierdlem76  47114  fourierdlem78  47116  fourierdlem79  47117  fourierdlem80  47118  fourierdlem81  47119  fourierdlem84  47122  fourierdlem88  47126  fourierdlem89  47127  fourierdlem90  47128  fourierdlem91  47129  fourierdlem100  47138  fourierdlem103  47141  fourierdlem104  47142  fourierdlem107  47145  fourierdlem111  47149  fourierdlem112  47150  etransclem18  47184  etransclem46  47212  rrxsnicc  47232  hoidmv1lelem1  47523  hoidmv1lelem3  47525  hoidmvlelem1  47527  hoidmvlelem2  47528  hoidmvlelem4  47530