Theorem iccssre 13465

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 13448	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑥 ∈ (𝐴[,]𝐵) ↔ (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵)))
2	1	biimp3a 1468	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵))
3	2	simp1d 1141	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ∈ ℝ)
4	3	3expia 1120	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑥 ∈ (𝐴[,]𝐵) → 𝑥 ∈ ℝ))
5	4	ssrdv 4000	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086   ∈ wcel 2105   ⊆ wss 3962   class class class wbr 5147  (class class class)co 7430  ℝcr 11151   ≤ cle 11293  [,]cicc 13386

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-cnex 11208  ax-resscn 11209  ax-pre-lttri 11226  ax-pre-lttrn 11227

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5582  df-po 5596  df-so 5597  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-ov 7433  df-oprab 7434  df-mpo 7435  df-er 8743  df-en 8984  df-dom 8985  df-sdom 8986  df-pnf 11294  df-mnf 11295  df-xr 11296  df-ltxr 11297  df-le 11298  df-icc 13390

This theorem is referenced by:  iccssred  13470  iccsupr  13478  iccsplit  13521  iccshftri  13523  iccshftli  13525  iccdili  13527  icccntri  13529  unitssre  13535  supicc  13537  supiccub  13538  supicclub  13539  icccld  24802  iccntr  24856  icccmplem2  24858  icccmplem3  24859  icccmp  24860  retopconn  24864  iccconn  24865  cnmpopc  24968  iihalf1cn  24972  iihalf1cnOLD  24973  iihalf2cn  24975  iihalf2cnOLD  24976  icoopnst  24982  iocopnst  24983  icchmeo  24984  icchmeoOLD  24985  xrhmeo  24990  icccvx  24994  cnheiborlem  24999  htpycc  25025  pcocn  25063  pcohtpylem  25065  pcopt  25068  pcopt2  25069  pcoass  25070  pcorevlem  25072  ivthlem2  25500  ivthlem3  25501  ivthicc  25506  evthicc  25507  ovolficcss  25517  ovolicc1  25564  ovolicc2  25570  ovolicc  25571  iccmbl  25614  ovolioo  25616  dyadss  25642  volcn  25654  volivth  25655  vitalilem2  25657  vitalilem4  25659  mbfimaicc  25679  mbfi1fseqlem4  25767  itgioo  25865  rollelem  26041  rolle  26042  cmvthOLD  26044  mvth  26045  dvlip  26046  c1liplem1  26049  c1lip1  26050  c1lip3  26052  dvgt0lem1  26055  dvgt0lem2  26056  dvgt0  26057  dvlt0  26058  dvge0  26059  dvle  26060  dvivthlem1  26061  dvivth  26063  dvne0  26064  lhop1lem  26066  dvcvx  26073  dvfsumleOLD  26075  dvfsumge  26076  dvfsumabs  26077  ftc1lem1  26090  ftc1a  26092  ftc1lem4  26094  ftc1lem5  26095  ftc1lem6  26096  ftc1  26097  ftc1cn  26098  ftc2  26099  ftc2ditglem  26100  ftc2ditg  26101  itgparts  26102  itgsubstlem  26103  itgpowd  26105  aalioulem3  26390  reeff1olem  26504  efcvx  26507  pilem3  26511  pige3ALT  26576  sinord  26590  recosf1o  26591  resinf1o  26592  efif1olem4  26601  asinrecl  26959  acosrecl  26960  emre  27063  pntlem3  27667  ttgcontlem1  28913  signsply0  34544  iblidicc  34585  ftc2re  34591  iccsconn  35232  iccllysconn  35234  cvmliftlem10  35278  ivthALT  36317  sin2h  37596  cos2h  37597  mblfinlem2  37644  ftc1cnnclem  37677  ftc1cnnc  37678  ftc1anclem7  37685  ftc1anc  37687  ftc2nc  37688  areacirclem2  37695  areacirclem3  37696  areacirclem4  37697  areacirc  37699  iccbnd  37826  icccmpALT  37827  arearect  43203  areaquad  43204  lhe4.4ex1a  44324  lefldiveq  45242  itgsin0pilem1  45905  ibliccsinexp  45906  iblioosinexp  45908  itgsinexplem1  45909  itgsinexp  45910  iblspltprt  45928  fourierdlem5  46067  fourierdlem9  46071  fourierdlem18  46080  fourierdlem24  46086  fourierdlem62  46123  fourierdlem66  46127  fourierdlem74  46135  fourierdlem75  46136  fourierdlem83  46144  fourierdlem87  46148  fourierdlem93  46154  fourierdlem95  46156  fourierdlem102  46163  fourierdlem103  46164  fourierdlem104  46165  fourierdlem112  46173  fourierdlem114  46175  sqwvfoura  46183  sqwvfourb  46184