Theorem iccssre 13397

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086   ∈ wcel 2109   ⊆ wss 3917   class class class wbr 5110  (class class class)co 7390  ℝcr 11074   ≤ cle 11216  [,]cicc 13316

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714  ax-cnex 11131  ax-resscn 11132  ax-pre-lttri 11149  ax-pre-lttrn 11150

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-nel 3031  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-po 5549  df-so 5550  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-ov 7393  df-oprab 7394  df-mpo 7395  df-er 8674  df-en 8922  df-dom 8923  df-sdom 8924  df-pnf 11217  df-mnf 11218  df-xr 11219  df-ltxr 11220  df-le 11221  df-icc 13320

This theorem is referenced by:  iccssred  13402  iccsupr  13410  iccsplit  13453  iccshftri  13455  iccshftli  13457  iccdili  13459  icccntri  13461  unitssre  13467  supicc  13469  supiccub  13470  supicclub  13471  icccld  24661  iccntr  24717  icccmplem2  24719  icccmplem3  24720  icccmp  24721  retopconn  24725  iccconn  24726  cnmpopc  24829  iihalf1cn  24833  iihalf1cnOLD  24834  iihalf2cn  24836  iihalf2cnOLD  24837  icoopnst  24843  iocopnst  24844  icchmeo  24845  icchmeoOLD  24846  xrhmeo  24851  icccvx  24855  cnheiborlem  24860  htpycc  24886  pcocn  24924  pcohtpylem  24926  pcopt  24929  pcopt2  24930  pcoass  24931  pcorevlem  24933  ivthlem2  25360  ivthlem3  25361  ivthicc  25366  evthicc  25367  ovolficcss  25377  ovolicc1  25424  ovolicc2  25430  ovolicc  25431  iccmbl  25474  ovolioo  25476  dyadss  25502  volcn  25514  volivth  25515  vitalilem2  25517  vitalilem4  25519  mbfimaicc  25539  mbfi1fseqlem4  25626  itgioo  25724  rollelem  25900  rolle  25901  cmvthOLD  25903  mvth  25904  dvlip  25905  c1liplem1  25908  c1lip1  25909  c1lip3  25911  dvgt0lem1  25914  dvgt0lem2  25915  dvgt0  25916  dvlt0  25917  dvge0  25918  dvle  25919  dvivthlem1  25920  dvivth  25922  dvne0  25923  lhop1lem  25925  dvcvx  25932  dvfsumleOLD  25934  dvfsumge  25935  dvfsumabs  25936  ftc1lem1  25949  ftc1a  25951  ftc1lem4  25953  ftc1lem5  25954  ftc1lem6  25955  ftc1  25956  ftc1cn  25957  ftc2  25958  ftc2ditglem  25959  ftc2ditg  25960  itgparts  25961  itgsubstlem  25962  itgpowd  25964  aalioulem3  26249  reeff1olem  26363  efcvx  26366  pilem3  26370  pige3ALT  26436  sinord  26450  recosf1o  26451  resinf1o  26452  efif1olem4  26461  asinrecl  26819  acosrecl  26820  emre  26923  pntlem3  27527  ttgcontlem1  28819  signsply0  34549  iblidicc  34590  ftc2re  34596  iccsconn  35242  iccllysconn  35244  cvmliftlem10  35288  ivthALT  36330  sin2h  37611  cos2h  37612  mblfinlem2  37659  ftc1cnnclem  37692  ftc1cnnc  37693  ftc1anclem7  37700  ftc1anc  37702  ftc2nc  37703  areacirclem2  37710  areacirclem3  37711  areacirclem4  37712  areacirc  37714  iccbnd  37841  icccmpALT  37842  arearect  43211  areaquad  43212  lhe4.4ex1a  44325  lefldiveq  45297  itgsin0pilem1  45955  ibliccsinexp  45956  iblioosinexp  45958  itgsinexplem1  45959  itgsinexp  45960  iblspltprt  45978  fourierdlem5  46117  fourierdlem9  46121  fourierdlem18  46130  fourierdlem24  46136  fourierdlem62  46173  fourierdlem66  46177  fourierdlem74  46185  fourierdlem75  46186  fourierdlem83  46194  fourierdlem87  46198  fourierdlem93  46204  fourierdlem95  46206  fourierdlem102  46213  fourierdlem103  46214  fourierdlem104  46215  fourierdlem112  46223  fourierdlem114  46225  sqwvfoura  46233  sqwvfourb  46234