Theorem iccssre 12126

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 12109	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑥 ∈ (𝐴[,]𝐵) ↔ (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵)))
2	1	biimp3a 1424	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵))
3	2	simp1d 1066	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ∈ ℝ)
4	3	3expia 1259	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑥 ∈ (𝐴[,]𝐵) → 𝑥 ∈ ℝ))
5	4	ssrdv 3574	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ)

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031   ∈ wcel 1977   ⊆ wss 3540   class class class wbr 4583  (class class class)co 6549  ℝcr 9814   ≤ cle 9954  [,]cicc 12049

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-cnex 9871  ax-resscn 9872  ax-pre-lttri 9889  ax-pre-lttrn 9890

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-po 4959  df-so 4960  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-er 7629  df-en 7842  df-dom 7843  df-sdom 7844  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-icc 12053

This theorem is referenced by:  iccsupr  12137  iccsplit  12176  iccshftri  12178  iccshftli  12180  iccdili  12182  icccntri  12184  unitssre  12190  supicc  12191  supiccub  12192  supicclub  12193  icccld  22380  iccntr  22432  icccmplem2  22434  icccmplem3  22435  icccmp  22436  retopcon  22440  iccconn  22441  cnmpt2pc  22535  iihalf1cn  22539  iihalf2cn  22541  icoopnst  22546  iocopnst  22547  icchmeo  22548  xrhmeo  22553  icccvx  22557  cnheiborlem  22561  htpycc  22587  pcocn  22625  pcohtpylem  22627  pcopt  22630  pcopt2  22631  pcoass  22632  pcorevlem  22634  ivthlem2  23028  ivthlem3  23029  ivthicc  23034  evthicc  23035  ovolficcss  23045  ovolicc1  23091  ovolicc2  23097  ovolicc  23098  iccmbl  23141  ovolioo  23143  dyadss  23168  volcn  23180  volivth  23181  vitalilem2  23184  vitalilem4  23186  mbfimaicc  23206  mbfi1fseqlem4  23291  itgioo  23388  rollelem  23556  rolle  23557  cmvth  23558  mvth  23559  dvlip  23560  c1liplem1  23563  c1lip1  23564  c1lip3  23566  dvgt0lem1  23569  dvgt0lem2  23570  dvgt0  23571  dvlt0  23572  dvge0  23573  dvle  23574  dvivthlem1  23575  dvivth  23577  dvne0  23578  lhop1lem  23580  dvcvx  23587  dvfsumle  23588  dvfsumge  23589  dvfsumabs  23590  ftc1lem1  23602  ftc1a  23604  ftc1lem4  23606  ftc1lem5  23607  ftc1lem6  23608  ftc1  23609  ftc1cn  23610  ftc2  23611  ftc2ditglem  23612  ftc2ditg  23613  itgparts  23614  itgsubstlem  23615  aalioulem3  23893  reeff1olem  24004  efcvx  24007  pilem3  24011  pige3  24073  sinord  24084  recosf1o  24085  resinf1o  24086  efif1olem4  24095  asinrecl  24429  acosrecl  24430  emre  24532  pntlem3  25098  ttgcontlem1  25565  signsply0  29954  iccscon  30484  iccllyscon  30486  cvmliftlem10  30530  ivthALT  31500  sin2h  32569  cos2h  32570  mblfinlem2  32617  ftc1cnnclem  32653  ftc1cnnc  32654  ftc1anclem7  32661  ftc1anc  32663  ftc2nc  32664  areacirclem2  32671  areacirclem3  32672  areacirclem4  32673  areacirc  32675  iccbnd  32809  icccmpALT  32810  itgpowd  36819  arearect  36820  areaquad  36821  lhe4.4ex1a  37550  lefldiveq  38446  iccssred  38574  itgsin0pilem1  38841  ibliccsinexp  38842  iblioosinexp  38844  itgsinexplem1  38845  itgsinexp  38846  iblspltprt  38865  fourierdlem5  39005  fourierdlem9  39009  fourierdlem18  39018  fourierdlem24  39024  fourierdlem62  39061  fourierdlem66  39065  fourierdlem74  39073  fourierdlem75  39074  fourierdlem83  39082  fourierdlem87  39086  fourierdlem93  39092  fourierdlem95  39094  fourierdlem102  39101  fourierdlem103  39102  fourierdlem104  39103  fourierdlem112  39111  fourierdlem114  39113  sqwvfoura  39121  sqwvfourb  39122