Theorem iccssre 13373

Description: A closed real interval is a set of reals. (Contributed by FL, 6-Jun-2007.) (Proof shortened by Paul Chapman, 21-Jan-2008.)

Assertion

Ref	Expression
iccssre	⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ)

Proof of Theorem iccssre

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		elicc2 13355	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑥 ∈ (𝐴[,]𝐵) ↔ (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵)))
2	1	biimp3a 1472	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵))
3	2	simp1d 1143	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ∈ ℝ)
4	3	3expia 1122	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑥 ∈ (𝐴[,]𝐵) → 𝑥 ∈ ℝ))
5	4	ssrdv 3928	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087   ∈ wcel 2114   ⊆ wss 3890   class class class wbr 5086  (class class class)co 7360  ℝcr 11028   ≤ cle 11171  [,]cicc 13292

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pow 5302  ax-pr 5370  ax-un 7682  ax-cnex 11085  ax-resscn 11086  ax-pre-lttri 11103  ax-pre-lttrn 11104

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5519  df-po 5532  df-so 5533  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-ov 7363  df-oprab 7364  df-mpo 7365  df-er 8636  df-en 8887  df-dom 8888  df-sdom 8889  df-pnf 11172  df-mnf 11173  df-xr 11174  df-ltxr 11175  df-le 11176  df-icc 13296

This theorem is referenced by:  iccssred  13378  iccsupr  13386  iccsplit  13429  iccshftri  13431  iccshftli  13433  iccdili  13435  icccntri  13437  unitssre  13443  supicc  13445  supiccub  13446  supicclub  13447  icccld  24741  iccntr  24797  icccmplem2  24799  icccmplem3  24800  icccmp  24801  retopconn  24805  iccconn  24806  cnmpopc  24905  iihalf1cn  24909  iihalf2cn  24911  icoopnst  24916  iocopnst  24917  icchmeo  24918  xrhmeo  24923  icccvx  24927  cnheiborlem  24931  htpycc  24957  pcocn  24994  pcohtpylem  24996  pcopt  24999  pcopt2  25000  pcoass  25001  pcorevlem  25003  ivthlem2  25429  ivthlem3  25430  ivthicc  25435  evthicc  25436  ovolficcss  25446  ovolicc1  25493  ovolicc2  25499  ovolicc  25500  iccmbl  25543  ovolioo  25545  dyadss  25571  volcn  25583  volivth  25584  vitalilem2  25586  vitalilem4  25588  mbfimaicc  25608  mbfi1fseqlem4  25695  itgioo  25793  rollelem  25966  rolle  25967  mvth  25969  dvlip  25970  c1liplem1  25973  c1lip1  25974  c1lip3  25976  dvgt0lem1  25979  dvgt0lem2  25980  dvgt0  25981  dvlt0  25982  dvge0  25983  dvle  25984  dvivthlem1  25985  dvivth  25987  dvne0  25988  lhop1lem  25990  dvcvx  25997  dvfsumge  25999  dvfsumabs  26000  ftc1lem1  26012  ftc1a  26014  ftc1lem4  26016  ftc1lem5  26017  ftc1lem6  26018  ftc1  26019  ftc1cn  26020  ftc2  26021  ftc2ditglem  26022  ftc2ditg  26023  itgparts  26024  itgsubstlem  26025  itgpowd  26027  aalioulem3  26311  reeff1olem  26424  efcvx  26427  pilem3  26431  pige3ALT  26497  sinord  26511  recosf1o  26512  resinf1o  26513  efif1olem4  26522  asinrecl  26879  acosrecl  26880  emre  26983  pntlem3  27586  ttgcontlem1  28967  signsply0  34711  iblidicc  34752  ftc2re  34758  iccsconn  35446  iccllysconn  35448  cvmliftlem10  35492  ivthALT  36533  sin2h  37945  cos2h  37946  mblfinlem2  37993  ftc1cnnclem  38026  ftc1cnnc  38027  ftc1anclem7  38034  ftc1anc  38036  ftc2nc  38037  areacirclem2  38044  areacirclem3  38045  areacirclem4  38046  areacirc  38048  iccbnd  38175  icccmpALT  38176  arearect  43661  areaquad  43662  lhe4.4ex1a  44774  lefldiveq  45743  itgsin0pilem1  46396  ibliccsinexp  46397  iblioosinexp  46399  itgsinexplem1  46400  itgsinexp  46401  iblspltprt  46419  fourierdlem5  46558  fourierdlem9  46562  fourierdlem18  46571  fourierdlem24  46577  fourierdlem62  46614  fourierdlem66  46618  fourierdlem74  46626  fourierdlem75  46627  fourierdlem83  46635  fourierdlem87  46639  fourierdlem93  46645  fourierdlem95  46647  fourierdlem102  46654  fourierdlem103  46655  fourierdlem104  46656  fourierdlem112  46664  fourierdlem114  46666  sqwvfoura  46674  sqwvfourb  46675