Theorem iccssre 13469

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087   ∈ wcel 2108   ⊆ wss 3951   class class class wbr 5143  (class class class)co 7431  ℝcr 11154   ≤ cle 11296  [,]cicc 13390

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-cnex 11211  ax-resscn 11212  ax-pre-lttri 11229  ax-pre-lttrn 11230

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-po 5592  df-so 5593  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-ov 7434  df-oprab 7435  df-mpo 7436  df-er 8745  df-en 8986  df-dom 8987  df-sdom 8988  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301  df-icc 13394

This theorem is referenced by:  iccssred  13474  iccsupr  13482  iccsplit  13525  iccshftri  13527  iccshftli  13529  iccdili  13531  icccntri  13533  unitssre  13539  supicc  13541  supiccub  13542  supicclub  13543  icccld  24787  iccntr  24843  icccmplem2  24845  icccmplem3  24846  icccmp  24847  retopconn  24851  iccconn  24852  cnmpopc  24955  iihalf1cn  24959  iihalf1cnOLD  24960  iihalf2cn  24962  iihalf2cnOLD  24963  icoopnst  24969  iocopnst  24970  icchmeo  24971  icchmeoOLD  24972  xrhmeo  24977  icccvx  24981  cnheiborlem  24986  htpycc  25012  pcocn  25050  pcohtpylem  25052  pcopt  25055  pcopt2  25056  pcoass  25057  pcorevlem  25059  ivthlem2  25487  ivthlem3  25488  ivthicc  25493  evthicc  25494  ovolficcss  25504  ovolicc1  25551  ovolicc2  25557  ovolicc  25558  iccmbl  25601  ovolioo  25603  dyadss  25629  volcn  25641  volivth  25642  vitalilem2  25644  vitalilem4  25646  mbfimaicc  25666  mbfi1fseqlem4  25753  itgioo  25851  rollelem  26027  rolle  26028  cmvthOLD  26030  mvth  26031  dvlip  26032  c1liplem1  26035  c1lip1  26036  c1lip3  26038  dvgt0lem1  26041  dvgt0lem2  26042  dvgt0  26043  dvlt0  26044  dvge0  26045  dvle  26046  dvivthlem1  26047  dvivth  26049  dvne0  26050  lhop1lem  26052  dvcvx  26059  dvfsumleOLD  26061  dvfsumge  26062  dvfsumabs  26063  ftc1lem1  26076  ftc1a  26078  ftc1lem4  26080  ftc1lem5  26081  ftc1lem6  26082  ftc1  26083  ftc1cn  26084  ftc2  26085  ftc2ditglem  26086  ftc2ditg  26087  itgparts  26088  itgsubstlem  26089  itgpowd  26091  aalioulem3  26376  reeff1olem  26490  efcvx  26493  pilem3  26497  pige3ALT  26562  sinord  26576  recosf1o  26577  resinf1o  26578  efif1olem4  26587  asinrecl  26945  acosrecl  26946  emre  27049  pntlem3  27653  ttgcontlem1  28899  signsply0  34566  iblidicc  34607  ftc2re  34613  iccsconn  35253  iccllysconn  35255  cvmliftlem10  35299  ivthALT  36336  sin2h  37617  cos2h  37618  mblfinlem2  37665  ftc1cnnclem  37698  ftc1cnnc  37699  ftc1anclem7  37706  ftc1anc  37708  ftc2nc  37709  areacirclem2  37716  areacirclem3  37717  areacirclem4  37718  areacirc  37720  iccbnd  37847  icccmpALT  37848  arearect  43227  areaquad  43228  lhe4.4ex1a  44348  lefldiveq  45304  itgsin0pilem1  45965  ibliccsinexp  45966  iblioosinexp  45968  itgsinexplem1  45969  itgsinexp  45970  iblspltprt  45988  fourierdlem5  46127  fourierdlem9  46131  fourierdlem18  46140  fourierdlem24  46146  fourierdlem62  46183  fourierdlem66  46187  fourierdlem74  46195  fourierdlem75  46196  fourierdlem83  46204  fourierdlem87  46208  fourierdlem93  46214  fourierdlem95  46216  fourierdlem102  46223  fourierdlem103  46224  fourierdlem104  46225  fourierdlem112  46233  fourierdlem114  46235  sqwvfoura  46243  sqwvfourb  46244