Theorem iccssre 12903

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1088   ∈ wcel 2114   ⊆ wss 3843   class class class wbr 5030  (class class class)co 7170  ℝcr 10614   ≤ cle 10754  [,]cicc 12824

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2162  ax-12 2179  ax-ext 2710  ax-sep 5167  ax-nul 5174  ax-pow 5232  ax-pr 5296  ax-un 7479  ax-cnex 10671  ax-resscn 10672  ax-pre-lttri 10689  ax-pre-lttrn 10690

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2075  df-mo 2540  df-eu 2570  df-clab 2717  df-cleq 2730  df-clel 2811  df-nfc 2881  df-ne 2935  df-nel 3039  df-ral 3058  df-rex 3059  df-rab 3062  df-v 3400  df-sbc 3681  df-csb 3791  df-dif 3846  df-un 3848  df-in 3850  df-ss 3860  df-nul 4212  df-if 4415  df-pw 4490  df-sn 4517  df-pr 4519  df-op 4523  df-uni 4797  df-br 5031  df-opab 5093  df-mpt 5111  df-id 5429  df-po 5442  df-so 5443  df-xp 5531  df-rel 5532  df-cnv 5533  df-co 5534  df-dm 5535  df-rn 5536  df-res 5537  df-ima 5538  df-iota 6297  df-fun 6341  df-fn 6342  df-f 6343  df-f1 6344  df-fo 6345  df-f1o 6346  df-fv 6347  df-ov 7173  df-oprab 7174  df-mpo 7175  df-er 8320  df-en 8556  df-dom 8557  df-sdom 8558  df-pnf 10755  df-mnf 10756  df-xr 10757  df-ltxr 10758  df-le 10759  df-icc 12828

This theorem is referenced by:  iccssred  12908  iccsupr  12916  iccsplit  12959  iccshftri  12961  iccshftli  12963  iccdili  12965  icccntri  12967  unitssre  12973  supicc  12975  supiccub  12976  supicclub  12977  icccld  23519  iccntr  23573  icccmplem2  23575  icccmplem3  23576  icccmp  23577  retopconn  23581  iccconn  23582  cnmpopc  23680  iihalf1cn  23684  iihalf2cn  23686  icoopnst  23691  iocopnst  23692  icchmeo  23693  xrhmeo  23698  icccvx  23702  cnheiborlem  23706  htpycc  23732  pcocn  23769  pcohtpylem  23771  pcopt  23774  pcopt2  23775  pcoass  23776  pcorevlem  23778  ivthlem2  24204  ivthlem3  24205  ivthicc  24210  evthicc  24211  ovolficcss  24221  ovolicc1  24268  ovolicc2  24274  ovolicc  24275  iccmbl  24318  ovolioo  24320  dyadss  24346  volcn  24358  volivth  24359  vitalilem2  24361  vitalilem4  24363  mbfimaicc  24383  mbfi1fseqlem4  24471  itgioo  24568  rollelem  24741  rolle  24742  cmvth  24743  mvth  24744  dvlip  24745  c1liplem1  24748  c1lip1  24749  c1lip3  24751  dvgt0lem1  24754  dvgt0lem2  24755  dvgt0  24756  dvlt0  24757  dvge0  24758  dvle  24759  dvivthlem1  24760  dvivth  24762  dvne0  24763  lhop1lem  24765  dvcvx  24772  dvfsumle  24773  dvfsumge  24774  dvfsumabs  24775  ftc1lem1  24787  ftc1a  24789  ftc1lem4  24791  ftc1lem5  24792  ftc1lem6  24793  ftc1  24794  ftc1cn  24795  ftc2  24796  ftc2ditglem  24797  ftc2ditg  24798  itgparts  24799  itgsubstlem  24800  itgpowd  24802  aalioulem3  25082  reeff1olem  25193  efcvx  25196  pilem3  25200  pige3ALT  25264  sinord  25278  recosf1o  25279  resinf1o  25280  efif1olem4  25289  asinrecl  25640  acosrecl  25641  emre  25743  pntlem3  26345  ttgcontlem1  26831  signsply0  32100  iblidicc  32142  ftc2re  32148  iccsconn  32781  iccllysconn  32783  cvmliftlem10  32827  ivthALT  34162  sin2h  35390  cos2h  35391  mblfinlem2  35438  ftc1cnnclem  35471  ftc1cnnc  35472  ftc1anclem7  35479  ftc1anc  35481  ftc2nc  35482  areacirclem2  35489  areacirclem3  35490  areacirclem4  35491  areacirc  35493  iccbnd  35621  icccmpALT  35622  arearect  40618  areaquad  40619  lhe4.4ex1a  41485  lefldiveq  42369  itgsin0pilem1  43033  ibliccsinexp  43034  iblioosinexp  43036  itgsinexplem1  43037  itgsinexp  43038  iblspltprt  43056  fourierdlem5  43195  fourierdlem9  43199  fourierdlem18  43208  fourierdlem24  43214  fourierdlem62  43251  fourierdlem66  43255  fourierdlem74  43263  fourierdlem75  43264  fourierdlem83  43272  fourierdlem87  43276  fourierdlem93  43282  fourierdlem95  43284  fourierdlem102  43291  fourierdlem103  43292  fourierdlem104  43293  fourierdlem112  43301  fourierdlem114  43303  sqwvfoura  43311  sqwvfourb  43312