Theorem iccssre 13541

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103   ∈ wcel 2145   ⊆ wss 3899   class class class wbr 5103  (class class class)co 7412  ℝcr 11180   ≤ cle 11325  [,]cicc 13460

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7740  ax-cnex 11237  ax-resscn 11238  ax-pre-lttri 11255  ax-pre-lttrn 11256

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 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3063  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5546  df-po 5559  df-so 5560  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6487  df-fun 6533  df-fn 6534  df-f 6535  df-f1 6536  df-fo 6537  df-f1o 6538  df-fv 6539  df-ov 7415  df-oprab 7416  df-mpo 7417  df-er 8701  df-en 8958  df-dom 8959  df-sdom 8960  df-pnf 11326  df-mnf 11327  df-xr 11328  df-ltxr 11329  df-le 11330  df-icc 13464

This theorem is used by:  iccssred  13546  iccsupr  13554  iccsplit  13597  iccshftri  13599  iccshftli  13601  iccdili  13603  icccntri  13605  unitssre  13611  supicc  13613  supiccub  13614  supicclub  13615  icccld  25065  iccntr  25121  icccmplem2  25123  icccmplem3  25124  icccmp  25125  retopconn  25129  iccconn  25130  cnmpopc  25229  iihalf1cn  25233  iihalf2cn  25235  icoopnst  25240  iocopnst  25241  icchmeo  25242  xrhmeo  25247  icccvx  25251  cnheiborlem  25255  htpycc  25281  pcocn  25318  pcohtpylem  25320  pcopt  25323  pcopt2  25324  pcoass  25325  pcorevlem  25327  ivthlem2  25753  ivthlem3  25754  ivthicc  25759  evthicc  25760  ovolficcss  25770  ovolicc1  25817  ovolicc2  25823  ovolicc  25824  iccmbl  25867  ovolioo  25869  dyadss  25895  volcn  25907  volivth  25908  vitalilem2  25910  vitalilem4  25912  mbfimaicc  25932  mbfi1fseqlem4  26019  itgioo  26116  rollelem  26289  rolle  26290  mvth  26292  dvlip  26293  c1liplem1  26296  c1lip1  26297  c1lip3  26299  dvgt0lem1  26302  dvgt0lem2  26303  dvgt0  26304  dvlt0  26305  dvge0  26306  dvle  26307  dvivthlem1  26308  dvivth  26310  dvne0  26311  lhop1lem  26313  dvcvx  26320  dvfsumge  26322  dvfsumabs  26323  ftc1lem1  26335  ftc1a  26337  ftc1lem4  26339  ftc1lem5  26340  ftc1lem6  26341  ftc1  26342  ftc1cn  26343  ftc2  26344  ftc2ditglem  26345  ftc2ditg  26346  itgparts  26347  itgsubstlem  26348  itgpowd  26350  aalioulem3  26643  reeff1olem  26755  efcvx  26758  pilem3  26762  pige3ALT  26830  sinord  26844  recosf1o  26845  resinf1o  26846  efif1olem4  26855  asinrecl  27212  acosrecl  27213  emre  27315  pntlem3  27918  ttgcontlem1  29444  signsply0  35163  iblidicc  35204  ftc2re  35210  iccsconn  35982  iccllysconn  35984  cvmliftlem10  36028  ivthALT  37093  sin2h  38501  cos2h  38502  mblfinlem2  38544  ftc1cnnclem  38577  ftc1cnnc  38578  ftc1anclem7  38585  ftc1anc  38587  ftc2nc  38588  areacirclem2  38595  areacirclem3  38596  areacirclem4  38597  areacirc  38599  iccbnd  38742  icccmpALT  38743  arearect  44175  areaquad  44176  lhe4.4ex1a  45272  lefldiveq  46251  itgsin0pilem1  46904  ibliccsinexp  46905  iblioosinexp  46907  itgsinexplem1  46908  itgsinexp  46909  iblspltprt  46927  fourierdlem5  47066  fourierdlem9  47070  fourierdlem18  47079  fourierdlem24  47085  fourierdlem62  47122  fourierdlem66  47126  fourierdlem74  47134  fourierdlem75  47135  fourierdlem83  47143  fourierdlem87  47147  fourierdlem93  47153  fourierdlem95  47155  fourierdlem102  47162  fourierdlem103  47163  fourierdlem104  47164  fourierdlem112  47172  fourierdlem114  47174  sqwvfoura  47182  sqwvfourb  47183