Theorem iccssre 13326

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086   ∈ wcel 2111   ⊆ wss 3902   class class class wbr 5091  (class class class)co 7346  ℝcr 11002   ≤ cle 11144  [,]cicc 13245

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 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5234  ax-nul 5244  ax-pow 5303  ax-pr 5370  ax-un 7668  ax-cnex 11059  ax-resscn 11060  ax-pre-lttri 11077  ax-pre-lttrn 11078

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-nel 3033  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-sbc 3742  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4476  df-pw 4552  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5092  df-opab 5154  df-mpt 5173  df-id 5511  df-po 5524  df-so 5525  df-xp 5622  df-rel 5623  df-cnv 5624  df-co 5625  df-dm 5626  df-rn 5627  df-res 5628  df-ima 5629  df-iota 6437  df-fun 6483  df-fn 6484  df-f 6485  df-f1 6486  df-fo 6487  df-f1o 6488  df-fv 6489  df-ov 7349  df-oprab 7350  df-mpo 7351  df-er 8622  df-en 8870  df-dom 8871  df-sdom 8872  df-pnf 11145  df-mnf 11146  df-xr 11147  df-ltxr 11148  df-le 11149  df-icc 13249

This theorem is referenced by:  iccssred  13331  iccsupr  13339  iccsplit  13382  iccshftri  13384  iccshftli  13386  iccdili  13388  icccntri  13390  unitssre  13396  supicc  13398  supiccub  13399  supicclub  13400  icccld  24679  iccntr  24735  icccmplem2  24737  icccmplem3  24738  icccmp  24739  retopconn  24743  iccconn  24744  cnmpopc  24847  iihalf1cn  24851  iihalf1cnOLD  24852  iihalf2cn  24854  iihalf2cnOLD  24855  icoopnst  24861  iocopnst  24862  icchmeo  24863  icchmeoOLD  24864  xrhmeo  24869  icccvx  24873  cnheiborlem  24878  htpycc  24904  pcocn  24942  pcohtpylem  24944  pcopt  24947  pcopt2  24948  pcoass  24949  pcorevlem  24951  ivthlem2  25378  ivthlem3  25379  ivthicc  25384  evthicc  25385  ovolficcss  25395  ovolicc1  25442  ovolicc2  25448  ovolicc  25449  iccmbl  25492  ovolioo  25494  dyadss  25520  volcn  25532  volivth  25533  vitalilem2  25535  vitalilem4  25537  mbfimaicc  25557  mbfi1fseqlem4  25644  itgioo  25742  rollelem  25918  rolle  25919  cmvthOLD  25921  mvth  25922  dvlip  25923  c1liplem1  25926  c1lip1  25927  c1lip3  25929  dvgt0lem1  25932  dvgt0lem2  25933  dvgt0  25934  dvlt0  25935  dvge0  25936  dvle  25937  dvivthlem1  25938  dvivth  25940  dvne0  25941  lhop1lem  25943  dvcvx  25950  dvfsumleOLD  25952  dvfsumge  25953  dvfsumabs  25954  ftc1lem1  25967  ftc1a  25969  ftc1lem4  25971  ftc1lem5  25972  ftc1lem6  25973  ftc1  25974  ftc1cn  25975  ftc2  25976  ftc2ditglem  25977  ftc2ditg  25978  itgparts  25979  itgsubstlem  25980  itgpowd  25982  aalioulem3  26267  reeff1olem  26381  efcvx  26384  pilem3  26388  pige3ALT  26454  sinord  26468  recosf1o  26469  resinf1o  26470  efif1olem4  26479  asinrecl  26837  acosrecl  26838  emre  26941  pntlem3  27545  ttgcontlem1  28861  signsply0  34559  iblidicc  34600  ftc2re  34606  iccsconn  35280  iccllysconn  35282  cvmliftlem10  35326  ivthALT  36368  sin2h  37649  cos2h  37650  mblfinlem2  37697  ftc1cnnclem  37730  ftc1cnnc  37731  ftc1anclem7  37738  ftc1anc  37740  ftc2nc  37741  areacirclem2  37748  areacirclem3  37749  areacirclem4  37750  areacirc  37752  iccbnd  37879  icccmpALT  37880  arearect  43247  areaquad  43248  lhe4.4ex1a  44361  lefldiveq  45332  itgsin0pilem1  45987  ibliccsinexp  45988  iblioosinexp  45990  itgsinexplem1  45991  itgsinexp  45992  iblspltprt  46010  fourierdlem5  46149  fourierdlem9  46153  fourierdlem18  46162  fourierdlem24  46168  fourierdlem62  46205  fourierdlem66  46209  fourierdlem74  46217  fourierdlem75  46218  fourierdlem83  46226  fourierdlem87  46230  fourierdlem93  46236  fourierdlem95  46238  fourierdlem102  46245  fourierdlem103  46246  fourierdlem104  46247  fourierdlem112  46255  fourierdlem114  46257  sqwvfoura  46265  sqwvfourb  46266