Theorem iccssre 13587

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103   ∈ wcel 2147   ⊆ wss 3900   class class class wbr 5106  (class class class)co 7443  ℝcr 11226   ≤ cle 11371  [,]cicc 13506

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5252  ax-nul 5263  ax-pow 5331  ax-pr 5395  ax-un 7775  ax-cnex 11283  ax-resscn 11284  ax-pre-lttri 11301  ax-pre-lttrn 11302

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3066  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5171  df-mpt 5190  df-id 5550  df-po 5563  df-so 5564  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6512  df-fun 6560  df-fn 6561  df-f 6562  df-f1 6563  df-fo 6564  df-f1o 6565  df-fv 6566  df-ov 7446  df-oprab 7447  df-mpo 7448  df-er 8745  df-en 9002  df-dom 9003  df-sdom 9004  df-pnf 11372  df-mnf 11373  df-xr 11374  df-ltxr 11375  df-le 11376  df-icc 13510

This theorem is used by:  iccssred  13592  iccsupr  13600  iccsplit  13643  iccshftri  13645  iccshftli  13647  iccdili  13649  icccntri  13651  unitssre  13657  supicc  13659  supiccub  13660  supicclub  13661  icccld  25115  iccntr  25171  icccmplem2  25173  icccmplem3  25174  icccmp  25175  retopconn  25179  iccconn  25180  cnmpopc  25279  iihalf1cn  25283  iihalf2cn  25285  icoopnst  25290  iocopnst  25291  icchmeo  25292  xrhmeo  25297  icccvx  25301  cnheiborlem  25305  htpycc  25331  pcocn  25368  pcohtpylem  25370  pcopt  25373  pcopt2  25374  pcoass  25375  pcorevlem  25377  ivthlem2  25803  ivthlem3  25804  ivthicc  25809  evthicc  25810  ovolficcss  25820  ovolicc1  25867  ovolicc2  25873  ovolicc  25874  iccmbl  25917  ovolioo  25919  dyadss  25945  volcn  25957  volivth  25958  vitalilem2  25960  vitalilem4  25962  mbfimaicc  25982  mbfi1fseqlem4  26069  itgioo  26166  rollelem  26339  rolle  26340  mvth  26342  dvlip  26343  c1liplem1  26346  c1lip1  26347  c1lip3  26349  dvgt0lem1  26352  dvgt0lem2  26353  dvgt0  26354  dvlt0  26355  dvge0  26356  dvle  26357  dvivthlem1  26358  dvivth  26360  dvne0  26361  lhop1lem  26363  dvcvx  26370  dvfsumge  26372  dvfsumabs  26373  ftc1lem1  26385  ftc1a  26387  ftc1lem4  26389  ftc1lem5  26390  ftc1lem6  26391  ftc1  26392  ftc1cn  26393  ftc2  26394  ftc2ditglem  26395  ftc2ditg  26396  itgparts  26397  itgsubstlem  26398  itgpowd  26400  aalioulem3  26691  reeff1olem  26803  efcvx  26806  pilem3  26810  pige3ALT  26878  sinord  26892  recosf1o  26893  resinf1o  26894  efif1olem4  26903  asinrecl  27260  acosrecl  27261  emre  27363  pntlem3  27966  ttgcontlem1  29492  signsply0  35250  iblidicc  35291  ftc2re  35297  iccsconn  36180  iccllysconn  36182  cvmliftlem10  36226  ivthALT  37301  sin2h  38725  cos2h  38726  mblfinlem2  38768  ftc1cnnclem  38801  ftc1cnnc  38802  ftc1anclem7  38809  ftc1anc  38811  ftc2nc  38812  areacirclem2  38819  areacirclem3  38820  areacirclem4  38821  areacirc  38823  iccbnd  38966  icccmpALT  38967  arearect  44409  areaquad  44410  lhe4.4ex1a  45505  lefldiveq  46513  itgsin0pilem1  47165  ibliccsinexp  47166  iblioosinexp  47168  itgsinexplem1  47169  itgsinexp  47170  iblspltprt  47188  fourierdlem5  47327  fourierdlem9  47331  fourierdlem18  47340  fourierdlem24  47346  fourierdlem62  47383  fourierdlem66  47387  fourierdlem74  47395  fourierdlem75  47396  fourierdlem83  47404  fourierdlem87  47408  fourierdlem93  47414  fourierdlem95  47416  fourierdlem102  47423  fourierdlem103  47424  fourierdlem104  47425  fourierdlem112  47433  fourierdlem114  47435  sqwvfoura  47443  sqwvfourb  47444