Theorem iccssre 12821

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083   ∈ wcel 2114   ⊆ wss 3938   class class class wbr 5068  (class class class)co 7158  ℝcr 10538   ≤ cle 10678  [,]cicc 12744

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 2795  ax-sep 5205  ax-nul 5212  ax-pow 5268  ax-pr 5332  ax-un 7463  ax-cnex 10595  ax-resscn 10596  ax-pre-lttri 10613  ax-pre-lttrn 10614

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 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ne 3019  df-nel 3126  df-ral 3145  df-rex 3146  df-rab 3149  df-v 3498  df-sbc 3775  df-csb 3886  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-pw 4543  df-sn 4570  df-pr 4572  df-op 4576  df-uni 4841  df-br 5069  df-opab 5131  df-mpt 5149  df-id 5462  df-po 5476  df-so 5477  df-xp 5563  df-rel 5564  df-cnv 5565  df-co 5566  df-dm 5567  df-rn 5568  df-res 5569  df-ima 5570  df-iota 6316  df-fun 6359  df-fn 6360  df-f 6361  df-f1 6362  df-fo 6363  df-f1o 6364  df-fv 6365  df-ov 7161  df-oprab 7162  df-mpo 7163  df-er 8291  df-en 8512  df-dom 8513  df-sdom 8514  df-pnf 10679  df-mnf 10680  df-xr 10681  df-ltxr 10682  df-le 10683  df-icc 12748

This theorem is referenced by:  iccsupr  12833  iccsplit  12874  iccshftri  12876  iccshftli  12878  iccdili  12880  icccntri  12882  unitssre  12888  supicc  12889  supiccub  12890  supicclub  12891  icccld  23377  iccntr  23431  icccmplem2  23433  icccmplem3  23434  icccmp  23435  retopconn  23439  iccconn  23440  cnmpopc  23534  iihalf1cn  23538  iihalf2cn  23540  icoopnst  23545  iocopnst  23546  icchmeo  23547  xrhmeo  23552  icccvx  23556  cnheiborlem  23560  htpycc  23586  pcocn  23623  pcohtpylem  23625  pcopt  23628  pcopt2  23629  pcoass  23630  pcorevlem  23632  ivthlem2  24055  ivthlem3  24056  ivthicc  24061  evthicc  24062  ovolficcss  24072  ovolicc1  24119  ovolicc2  24125  ovolicc  24126  iccmbl  24169  ovolioo  24171  dyadss  24197  volcn  24209  volivth  24210  vitalilem2  24212  vitalilem4  24214  mbfimaicc  24234  mbfi1fseqlem4  24321  itgioo  24418  rollelem  24588  rolle  24589  cmvth  24590  mvth  24591  dvlip  24592  c1liplem1  24595  c1lip1  24596  c1lip3  24598  dvgt0lem1  24601  dvgt0lem2  24602  dvgt0  24603  dvlt0  24604  dvge0  24605  dvle  24606  dvivthlem1  24607  dvivth  24609  dvne0  24610  lhop1lem  24612  dvcvx  24619  dvfsumle  24620  dvfsumge  24621  dvfsumabs  24622  ftc1lem1  24634  ftc1a  24636  ftc1lem4  24638  ftc1lem5  24639  ftc1lem6  24640  ftc1  24641  ftc1cn  24642  ftc2  24643  ftc2ditglem  24644  ftc2ditg  24645  itgparts  24646  itgsubstlem  24647  aalioulem3  24925  reeff1olem  25036  efcvx  25039  pilem3  25043  pige3ALT  25107  sinord  25120  recosf1o  25121  resinf1o  25122  efif1olem4  25131  asinrecl  25482  acosrecl  25483  emre  25585  pntlem3  26187  ttgcontlem1  26673  signsply0  31823  iblidicc  31865  ftc2re  31871  iccsconn  32497  iccllysconn  32499  cvmliftlem10  32543  ivthALT  33685  sin2h  34884  cos2h  34885  mblfinlem2  34932  ftc1cnnclem  34967  ftc1cnnc  34968  ftc1anclem7  34975  ftc1anc  34977  ftc2nc  34978  areacirclem2  34985  areacirclem3  34986  areacirclem4  34987  areacirc  34989  iccbnd  35120  icccmpALT  35121  itgpowd  39828  arearect  39829  areaquad  39830  lhe4.4ex1a  40668  lefldiveq  41566  iccssred  41787  itgsin0pilem1  42242  ibliccsinexp  42243  iblioosinexp  42245  itgsinexplem1  42246  itgsinexp  42247  iblspltprt  42265  fourierdlem5  42404  fourierdlem9  42408  fourierdlem18  42417  fourierdlem24  42423  fourierdlem62  42460  fourierdlem66  42464  fourierdlem74  42472  fourierdlem75  42473  fourierdlem83  42481  fourierdlem87  42485  fourierdlem93  42491  fourierdlem95  42493  fourierdlem102  42500  fourierdlem103  42501  fourierdlem104  42502  fourierdlem112  42510  fourierdlem114  42512  sqwvfoura  42520  sqwvfourb  42521