Theorem iccssre 13451

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 13434	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑥 ∈ (𝐴[,]𝐵) ↔ (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵)))
2	1	biimp3a 1470	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵))
3	2	simp1d 1142	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ∈ ℝ)
4	3	3expia 1121	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑥 ∈ (𝐴[,]𝐵) → 𝑥 ∈ ℝ))
5	4	ssrdv 3969	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086   ∈ wcel 2107   ⊆ wss 3931   class class class wbr 5123  (class class class)co 7413  ℝcr 11136   ≤ cle 11278  [,]cicc 13372

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706  ax-sep 5276  ax-nul 5286  ax-pow 5345  ax-pr 5412  ax-un 7737  ax-cnex 11193  ax-resscn 11194  ax-pre-lttri 11211  ax-pre-lttrn 11212

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2808  df-nfc 2884  df-ne 2932  df-nel 3036  df-ral 3051  df-rex 3060  df-rab 3420  df-v 3465  df-sbc 3771  df-csb 3880  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4888  df-br 5124  df-opab 5186  df-mpt 5206  df-id 5558  df-po 5572  df-so 5573  df-xp 5671  df-rel 5672  df-cnv 5673  df-co 5674  df-dm 5675  df-rn 5676  df-res 5677  df-ima 5678  df-iota 6494  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-ov 7416  df-oprab 7417  df-mpo 7418  df-er 8727  df-en 8968  df-dom 8969  df-sdom 8970  df-pnf 11279  df-mnf 11280  df-xr 11281  df-ltxr 11282  df-le 11283  df-icc 13376

This theorem is referenced by:  iccssred  13456  iccsupr  13464  iccsplit  13507  iccshftri  13509  iccshftli  13511  iccdili  13513  icccntri  13515  unitssre  13521  supicc  13523  supiccub  13524  supicclub  13525  icccld  24724  iccntr  24780  icccmplem2  24782  icccmplem3  24783  icccmp  24784  retopconn  24788  iccconn  24789  cnmpopc  24892  iihalf1cn  24896  iihalf1cnOLD  24897  iihalf2cn  24899  iihalf2cnOLD  24900  icoopnst  24906  iocopnst  24907  icchmeo  24908  icchmeoOLD  24909  xrhmeo  24914  icccvx  24918  cnheiborlem  24923  htpycc  24949  pcocn  24987  pcohtpylem  24989  pcopt  24992  pcopt2  24993  pcoass  24994  pcorevlem  24996  ivthlem2  25424  ivthlem3  25425  ivthicc  25430  evthicc  25431  ovolficcss  25441  ovolicc1  25488  ovolicc2  25494  ovolicc  25495  iccmbl  25538  ovolioo  25540  dyadss  25566  volcn  25578  volivth  25579  vitalilem2  25581  vitalilem4  25583  mbfimaicc  25603  mbfi1fseqlem4  25690  itgioo  25788  rollelem  25964  rolle  25965  cmvthOLD  25967  mvth  25968  dvlip  25969  c1liplem1  25972  c1lip1  25973  c1lip3  25975  dvgt0lem1  25978  dvgt0lem2  25979  dvgt0  25980  dvlt0  25981  dvge0  25982  dvle  25983  dvivthlem1  25984  dvivth  25986  dvne0  25987  lhop1lem  25989  dvcvx  25996  dvfsumleOLD  25998  dvfsumge  25999  dvfsumabs  26000  ftc1lem1  26013  ftc1a  26015  ftc1lem4  26017  ftc1lem5  26018  ftc1lem6  26019  ftc1  26020  ftc1cn  26021  ftc2  26022  ftc2ditglem  26023  ftc2ditg  26024  itgparts  26025  itgsubstlem  26026  itgpowd  26028  aalioulem3  26313  reeff1olem  26427  efcvx  26430  pilem3  26434  pige3ALT  26499  sinord  26513  recosf1o  26514  resinf1o  26515  efif1olem4  26524  asinrecl  26882  acosrecl  26883  emre  26986  pntlem3  27590  ttgcontlem1  28831  signsply0  34541  iblidicc  34582  ftc2re  34588  iccsconn  35228  iccllysconn  35230  cvmliftlem10  35274  ivthALT  36311  sin2h  37592  cos2h  37593  mblfinlem2  37640  ftc1cnnclem  37673  ftc1cnnc  37674  ftc1anclem7  37681  ftc1anc  37683  ftc2nc  37684  areacirclem2  37691  areacirclem3  37692  areacirclem4  37693  areacirc  37695  iccbnd  37822  icccmpALT  37823  arearect  43205  areaquad  43206  lhe4.4ex1a  44320  lefldiveq  45276  itgsin0pilem1  45937  ibliccsinexp  45938  iblioosinexp  45940  itgsinexplem1  45941  itgsinexp  45942  iblspltprt  45960  fourierdlem5  46099  fourierdlem9  46103  fourierdlem18  46112  fourierdlem24  46118  fourierdlem62  46155  fourierdlem66  46159  fourierdlem74  46167  fourierdlem75  46168  fourierdlem83  46176  fourierdlem87  46180  fourierdlem93  46186  fourierdlem95  46188  fourierdlem102  46195  fourierdlem103  46196  fourierdlem104  46197  fourierdlem112  46205  fourierdlem114  46207  sqwvfoura  46215  sqwvfourb  46216