Theorem iccssre 12819

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 12802	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑥 ∈ (𝐴[,]𝐵) ↔ (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵)))
2	1	biimp3a 1465	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵))
3	2	simp1d 1138	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ∈ ℝ)
4	3	3expia 1117	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑥 ∈ (𝐴[,]𝐵) → 𝑥 ∈ ℝ))
5	4	ssrdv 3973	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ)

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083   ∈ wcel 2114   ⊆ wss 3936   class class class wbr 5066  (class class class)co 7156  ℝcr 10536   ≤ cle 10676  [,]cicc 12742

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pow 5266  ax-pr 5330  ax-un 7461  ax-cnex 10593  ax-resscn 10594  ax-pre-lttri 10611  ax-pre-lttrn 10612

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-opab 5129  df-mpt 5147  df-id 5460  df-po 5474  df-so 5475  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568  df-iota 6314  df-fun 6357  df-fn 6358  df-f 6359  df-f1 6360  df-fo 6361  df-f1o 6362  df-fv 6363  df-ov 7159  df-oprab 7160  df-mpo 7161  df-er 8289  df-en 8510  df-dom 8511  df-sdom 8512  df-pnf 10677  df-mnf 10678  df-xr 10679  df-ltxr 10680  df-le 10681  df-icc 12746

This theorem is referenced by:  iccsupr  12831  iccsplit  12872  iccshftri  12874  iccshftli  12876  iccdili  12878  icccntri  12880  unitssre  12886  supicc  12887  supiccub  12888  supicclub  12889  icccld  23375  iccntr  23429  icccmplem2  23431  icccmplem3  23432  icccmp  23433  retopconn  23437  iccconn  23438  cnmpopc  23532  iihalf1cn  23536  iihalf2cn  23538  icoopnst  23543  iocopnst  23544  icchmeo  23545  xrhmeo  23550  icccvx  23554  cnheiborlem  23558  htpycc  23584  pcocn  23621  pcohtpylem  23623  pcopt  23626  pcopt2  23627  pcoass  23628  pcorevlem  23630  ivthlem2  24053  ivthlem3  24054  ivthicc  24059  evthicc  24060  ovolficcss  24070  ovolicc1  24117  ovolicc2  24123  ovolicc  24124  iccmbl  24167  ovolioo  24169  dyadss  24195  volcn  24207  volivth  24208  vitalilem2  24210  vitalilem4  24212  mbfimaicc  24232  mbfi1fseqlem4  24319  itgioo  24416  rollelem  24586  rolle  24587  cmvth  24588  mvth  24589  dvlip  24590  c1liplem1  24593  c1lip1  24594  c1lip3  24596  dvgt0lem1  24599  dvgt0lem2  24600  dvgt0  24601  dvlt0  24602  dvge0  24603  dvle  24604  dvivthlem1  24605  dvivth  24607  dvne0  24608  lhop1lem  24610  dvcvx  24617  dvfsumle  24618  dvfsumge  24619  dvfsumabs  24620  ftc1lem1  24632  ftc1a  24634  ftc1lem4  24636  ftc1lem5  24637  ftc1lem6  24638  ftc1  24639  ftc1cn  24640  ftc2  24641  ftc2ditglem  24642  ftc2ditg  24643  itgparts  24644  itgsubstlem  24645  aalioulem3  24923  reeff1olem  25034  efcvx  25037  pilem3  25041  pige3ALT  25105  sinord  25118  recosf1o  25119  resinf1o  25120  efif1olem4  25129  asinrecl  25480  acosrecl  25481  emre  25583  pntlem3  26185  ttgcontlem1  26671  signsply0  31821  iblidicc  31863  ftc2re  31869  iccsconn  32495  iccllysconn  32497  cvmliftlem10  32541  ivthALT  33683  sin2h  34897  cos2h  34898  mblfinlem2  34945  ftc1cnnclem  34980  ftc1cnnc  34981  ftc1anclem7  34988  ftc1anc  34990  ftc2nc  34991  areacirclem2  34998  areacirclem3  34999  areacirclem4  35000  areacirc  35002  iccbnd  35133  icccmpALT  35134  itgpowd  39841  arearect  39842  areaquad  39843  lhe4.4ex1a  40681  lefldiveq  41579  iccssred  41800  itgsin0pilem1  42255  ibliccsinexp  42256  iblioosinexp  42258  itgsinexplem1  42259  itgsinexp  42260  iblspltprt  42278  fourierdlem5  42417  fourierdlem9  42421  fourierdlem18  42430  fourierdlem24  42436  fourierdlem62  42473  fourierdlem66  42477  fourierdlem74  42485  fourierdlem75  42486  fourierdlem83  42494  fourierdlem87  42498  fourierdlem93  42504  fourierdlem95  42506  fourierdlem102  42513  fourierdlem103  42514  fourierdlem104  42515  fourierdlem112  42523  fourierdlem114  42525  sqwvfoura  42533  sqwvfourb  42534