Theorem iccssre 12807

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 12790	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑥 ∈ (𝐴[,]𝐵) ↔ (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵)))
2	1	biimp3a 1466	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵))
3	2	simp1d 1139	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ∈ ℝ)
4	3	3expia 1118	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑥 ∈ (𝐴[,]𝐵) → 𝑥 ∈ ℝ))
5	4	ssrdv 3921	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ)

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1084   ∈ wcel 2111   ⊆ wss 3881   class class class wbr 5030  (class class class)co 7135  ℝcr 10525   ≤ cle 10665  [,]cicc 12729

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441  ax-cnex 10582  ax-resscn 10583  ax-pre-lttri 10600  ax-pre-lttrn 10601

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-opab 5093  df-mpt 5111  df-id 5425  df-po 5438  df-so 5439  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332  df-ov 7138  df-oprab 7139  df-mpo 7140  df-er 8272  df-en 8493  df-dom 8494  df-sdom 8495  df-pnf 10666  df-mnf 10667  df-xr 10668  df-ltxr 10669  df-le 10670  df-icc 12733

This theorem is referenced by:  iccssred  12812  iccsupr  12820  iccsplit  12863  iccshftri  12865  iccshftli  12867  iccdili  12869  icccntri  12871  unitssre  12877  supicc  12879  supiccub  12880  supicclub  12881  icccld  23372  iccntr  23426  icccmplem2  23428  icccmplem3  23429  icccmp  23430  retopconn  23434  iccconn  23435  cnmpopc  23533  iihalf1cn  23537  iihalf2cn  23539  icoopnst  23544  iocopnst  23545  icchmeo  23546  xrhmeo  23551  icccvx  23555  cnheiborlem  23559  htpycc  23585  pcocn  23622  pcohtpylem  23624  pcopt  23627  pcopt2  23628  pcoass  23629  pcorevlem  23631  ivthlem2  24056  ivthlem3  24057  ivthicc  24062  evthicc  24063  ovolficcss  24073  ovolicc1  24120  ovolicc2  24126  ovolicc  24127  iccmbl  24170  ovolioo  24172  dyadss  24198  volcn  24210  volivth  24211  vitalilem2  24213  vitalilem4  24215  mbfimaicc  24235  mbfi1fseqlem4  24322  itgioo  24419  rollelem  24592  rolle  24593  cmvth  24594  mvth  24595  dvlip  24596  c1liplem1  24599  c1lip1  24600  c1lip3  24602  dvgt0lem1  24605  dvgt0lem2  24606  dvgt0  24607  dvlt0  24608  dvge0  24609  dvle  24610  dvivthlem1  24611  dvivth  24613  dvne0  24614  lhop1lem  24616  dvcvx  24623  dvfsumle  24624  dvfsumge  24625  dvfsumabs  24626  ftc1lem1  24638  ftc1a  24640  ftc1lem4  24642  ftc1lem5  24643  ftc1lem6  24644  ftc1  24645  ftc1cn  24646  ftc2  24647  ftc2ditglem  24648  ftc2ditg  24649  itgparts  24650  itgsubstlem  24651  itgpowd  24653  aalioulem3  24930  reeff1olem  25041  efcvx  25044  pilem3  25048  pige3ALT  25112  sinord  25126  recosf1o  25127  resinf1o  25128  efif1olem4  25137  asinrecl  25488  acosrecl  25489  emre  25591  pntlem3  26193  ttgcontlem1  26679  signsply0  31931  iblidicc  31973  ftc2re  31979  iccsconn  32608  iccllysconn  32610  cvmliftlem10  32654  ivthALT  33796  sin2h  35047  cos2h  35048  mblfinlem2  35095  ftc1cnnclem  35128  ftc1cnnc  35129  ftc1anclem7  35136  ftc1anc  35138  ftc2nc  35139  areacirclem2  35146  areacirclem3  35147  areacirclem4  35148  areacirc  35150  iccbnd  35278  icccmpALT  35279  arearect  40165  areaquad  40166  lhe4.4ex1a  41033  lefldiveq  41924  itgsin0pilem1  42592  ibliccsinexp  42593  iblioosinexp  42595  itgsinexplem1  42596  itgsinexp  42597  iblspltprt  42615  fourierdlem5  42754  fourierdlem9  42758  fourierdlem18  42767  fourierdlem24  42773  fourierdlem62  42810  fourierdlem66  42814  fourierdlem74  42822  fourierdlem75  42823  fourierdlem83  42831  fourierdlem87  42835  fourierdlem93  42841  fourierdlem95  42843  fourierdlem102  42850  fourierdlem103  42851  fourierdlem104  42852  fourierdlem112  42860  fourierdlem114  42862  sqwvfoura  42870  sqwvfourb  42871