Theorem iccssre 13359

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 13341	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑥 ∈ (𝐴[,]𝐵) ↔ (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵)))
2	1	biimp3a 1472	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵))
3	2	simp1d 1143	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ∈ ℝ)
4	3	3expia 1122	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑥 ∈ (𝐴[,]𝐵) → 𝑥 ∈ ℝ))
5	4	ssrdv 3941	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087   ∈ wcel 2114   ⊆ wss 3903   class class class wbr 5100  (class class class)co 7370  ℝcr 11039   ≤ cle 11181  [,]cicc 13278

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 5245  ax-nul 5255  ax-pow 5314  ax-pr 5381  ax-un 7692  ax-cnex 11096  ax-resscn 11097  ax-pre-lttri 11114  ax-pre-lttrn 11115

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 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5529  df-po 5542  df-so 5543  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-iota 6458  df-fun 6504  df-fn 6505  df-f 6506  df-f1 6507  df-fo 6508  df-f1o 6509  df-fv 6510  df-ov 7373  df-oprab 7374  df-mpo 7375  df-er 8647  df-en 8898  df-dom 8899  df-sdom 8900  df-pnf 11182  df-mnf 11183  df-xr 11184  df-ltxr 11185  df-le 11186  df-icc 13282

This theorem is referenced by:  iccssred  13364  iccsupr  13372  iccsplit  13415  iccshftri  13417  iccshftli  13419  iccdili  13421  icccntri  13423  unitssre  13429  supicc  13431  supiccub  13432  supicclub  13433  icccld  24727  iccntr  24783  icccmplem2  24785  icccmplem3  24786  icccmp  24787  retopconn  24791  iccconn  24792  cnmpopc  24895  iihalf1cn  24899  iihalf1cnOLD  24900  iihalf2cn  24902  iihalf2cnOLD  24903  icoopnst  24909  iocopnst  24910  icchmeo  24911  icchmeoOLD  24912  xrhmeo  24917  icccvx  24921  cnheiborlem  24926  htpycc  24952  pcocn  24990  pcohtpylem  24992  pcopt  24995  pcopt2  24996  pcoass  24997  pcorevlem  24999  ivthlem2  25426  ivthlem3  25427  ivthicc  25432  evthicc  25433  ovolficcss  25443  ovolicc1  25490  ovolicc2  25496  ovolicc  25497  iccmbl  25540  ovolioo  25542  dyadss  25568  volcn  25580  volivth  25581  vitalilem2  25583  vitalilem4  25585  mbfimaicc  25605  mbfi1fseqlem4  25692  itgioo  25790  rollelem  25966  rolle  25967  cmvthOLD  25969  mvth  25970  dvlip  25971  c1liplem1  25974  c1lip1  25975  c1lip3  25977  dvgt0lem1  25980  dvgt0lem2  25981  dvgt0  25982  dvlt0  25983  dvge0  25984  dvle  25985  dvivthlem1  25986  dvivth  25988  dvne0  25989  lhop1lem  25991  dvcvx  25998  dvfsumleOLD  26000  dvfsumge  26001  dvfsumabs  26002  ftc1lem1  26015  ftc1a  26017  ftc1lem4  26019  ftc1lem5  26020  ftc1lem6  26021  ftc1  26022  ftc1cn  26023  ftc2  26024  ftc2ditglem  26025  ftc2ditg  26026  itgparts  26027  itgsubstlem  26028  itgpowd  26030  aalioulem3  26315  reeff1olem  26429  efcvx  26432  pilem3  26436  pige3ALT  26502  sinord  26516  recosf1o  26517  resinf1o  26518  efif1olem4  26527  asinrecl  26885  acosrecl  26886  emre  26989  pntlem3  27593  ttgcontlem1  28975  signsply0  34735  iblidicc  34776  ftc2re  34782  iccsconn  35470  iccllysconn  35472  cvmliftlem10  35516  ivthALT  36557  sin2h  37890  cos2h  37891  mblfinlem2  37938  ftc1cnnclem  37971  ftc1cnnc  37972  ftc1anclem7  37979  ftc1anc  37981  ftc2nc  37982  areacirclem2  37989  areacirclem3  37990  areacirclem4  37991  areacirc  37993  iccbnd  38120  icccmpALT  38121  arearect  43601  areaquad  43602  lhe4.4ex1a  44714  lefldiveq  45683  itgsin0pilem1  46337  ibliccsinexp  46338  iblioosinexp  46340  itgsinexplem1  46341  itgsinexp  46342  iblspltprt  46360  fourierdlem5  46499  fourierdlem9  46503  fourierdlem18  46512  fourierdlem24  46518  fourierdlem62  46555  fourierdlem66  46559  fourierdlem74  46567  fourierdlem75  46568  fourierdlem83  46576  fourierdlem87  46580  fourierdlem93  46586  fourierdlem95  46588  fourierdlem102  46595  fourierdlem103  46596  fourierdlem104  46597  fourierdlem112  46605  fourierdlem114  46607  sqwvfoura  46615  sqwvfourb  46616