Theorem iccssre 13563

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 13545	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑥 ∈ (𝐴[,]𝐵) ↔ (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵)))
2	1	biimp3a 1498	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵))
3	2	simp1d 1160	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ∈ ℝ)
4	3	3expia 1139	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑥 ∈ (𝐴[,]𝐵) → 𝑥 ∈ ℝ))
5	4	ssrdv 3914	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103   ∈ wcel 2144   ⊆ wss 3895   class class class wbr 5102  (class class class)co 7420  ℝcr 11202   ≤ cle 11347  [,]cicc 13482

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7751  ax-cnex 11259  ax-resscn 11260  ax-pre-lttri 11277  ax-pre-lttrn 11278

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  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-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5545  df-po 5558  df-so 5559  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-ov 7423  df-oprab 7424  df-mpo 7425  df-er 8720  df-en 8977  df-dom 8978  df-sdom 8979  df-pnf 11348  df-mnf 11349  df-xr 11350  df-ltxr 11351  df-le 11352  df-icc 13486

This theorem is used by:  iccssred  13568  iccsupr  13576  iccsplit  13619  iccshftri  13621  iccshftli  13623  iccdili  13625  icccntri  13627  unitssre  13633  supicc  13635  supiccub  13636  supicclub  13637  icccld  25090  iccntr  25146  icccmplem2  25148  icccmplem3  25149  icccmp  25150  retopconn  25154  iccconn  25155  cnmpopc  25254  iihalf1cn  25258  iihalf2cn  25260  icoopnst  25265  iocopnst  25266  icchmeo  25267  xrhmeo  25272  icccvx  25276  cnheiborlem  25280  htpycc  25306  pcocn  25343  pcohtpylem  25345  pcopt  25348  pcopt2  25349  pcoass  25350  pcorevlem  25352  ivthlem2  25778  ivthlem3  25779  ivthicc  25784  evthicc  25785  ovolficcss  25795  ovolicc1  25842  ovolicc2  25848  ovolicc  25849  iccmbl  25892  ovolioo  25894  dyadss  25920  volcn  25932  volivth  25933  vitalilem2  25935  vitalilem4  25937  mbfimaicc  25957  mbfi1fseqlem4  26044  itgioo  26141  rollelem  26314  rolle  26315  mvth  26317  dvlip  26318  c1liplem1  26321  c1lip1  26322  c1lip3  26324  dvgt0lem1  26327  dvgt0lem2  26328  dvgt0  26329  dvlt0  26330  dvge0  26331  dvle  26332  dvivthlem1  26333  dvivth  26335  dvne0  26336  lhop1lem  26338  dvcvx  26345  dvfsumge  26347  dvfsumabs  26348  ftc1lem1  26360  ftc1a  26362  ftc1lem4  26364  ftc1lem5  26365  ftc1lem6  26366  ftc1  26367  ftc1cn  26368  ftc2  26369  ftc2ditglem  26370  ftc2ditg  26371  itgparts  26372  itgsubstlem  26373  itgpowd  26375  aalioulem3  26666  reeff1olem  26778  efcvx  26781  pilem3  26785  pige3ALT  26853  sinord  26867  recosf1o  26868  resinf1o  26869  efif1olem4  26878  asinrecl  27235  acosrecl  27236  emre  27338  pntlem3  27941  ttgcontlem1  29467  signsply0  35226  iblidicc  35267  ftc2re  35273  iccsconn  36099  iccllysconn  36101  cvmliftlem10  36145  ivthALT  37215  sin2h  38626  cos2h  38627  mblfinlem2  38669  ftc1cnnclem  38702  ftc1cnnc  38703  ftc1anclem7  38710  ftc1anc  38712  ftc2nc  38713  areacirclem2  38720  areacirclem3  38721  areacirclem4  38722  areacirc  38724  iccbnd  38867  icccmpALT  38868  arearect  44310  areaquad  44311  lhe4.4ex1a  45406  lefldiveq  46401  itgsin0pilem1  47053  ibliccsinexp  47054  iblioosinexp  47056  itgsinexplem1  47057  itgsinexp  47058  iblspltprt  47076  fourierdlem5  47215  fourierdlem9  47219  fourierdlem18  47228  fourierdlem24  47234  fourierdlem62  47271  fourierdlem66  47275  fourierdlem74  47283  fourierdlem75  47284  fourierdlem83  47292  fourierdlem87  47296  fourierdlem93  47302  fourierdlem95  47304  fourierdlem102  47311  fourierdlem103  47312  fourierdlem104  47313  fourierdlem112  47321  fourierdlem114  47323  sqwvfoura  47331  sqwvfourb  47332