MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  iccssre Structured version   Visualization version   GIF version

Theorem iccssre 12480
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.
StepHypRef Expression
1 elicc2 12463 . . . . 5 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑥 ∈ (𝐴[,]𝐵) ↔ (𝑥 ∈ ℝ ∧ 𝐴𝑥𝑥𝐵)))
21biimp3a 1586 . . . 4 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝑥 ∈ ℝ ∧ 𝐴𝑥𝑥𝐵))
32simp1d 1165 . . 3 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ∈ ℝ)
433expia 1143 . 2 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑥 ∈ (𝐴[,]𝐵) → 𝑥 ∈ ℝ))
54ssrdv 3815 1 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1100  wcel 2157  wss 3780   class class class wbr 4855  (class class class)co 6881  cr 10227  cle 10367  [,]cicc 12403
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-8 2159  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795  ax-sep 4986  ax-nul 4994  ax-pow 5046  ax-pr 5107  ax-un 7186  ax-cnex 10284  ax-resscn 10285  ax-pre-lttri 10302  ax-pre-lttrn 10303
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-mo 2635  df-eu 2642  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-ne 2990  df-nel 3093  df-ral 3112  df-rex 3113  df-rab 3116  df-v 3404  df-sbc 3645  df-csb 3740  df-dif 3783  df-un 3785  df-in 3787  df-ss 3794  df-nul 4128  df-if 4291  df-pw 4364  df-sn 4382  df-pr 4384  df-op 4388  df-uni 4642  df-br 4856  df-opab 4918  df-mpt 4935  df-id 5230  df-po 5243  df-so 5244  df-xp 5328  df-rel 5329  df-cnv 5330  df-co 5331  df-dm 5332  df-rn 5333  df-res 5334  df-ima 5335  df-iota 6071  df-fun 6110  df-fn 6111  df-f 6112  df-f1 6113  df-fo 6114  df-f1o 6115  df-fv 6116  df-ov 6884  df-oprab 6885  df-mpt2 6886  df-er 7986  df-en 8200  df-dom 8201  df-sdom 8202  df-pnf 10368  df-mnf 10369  df-xr 10370  df-ltxr 10371  df-le 10372  df-icc 12407
This theorem is referenced by:  iccsupr  12492  iccsplit  12535  iccshftri  12537  iccshftli  12539  iccdili  12541  icccntri  12543  unitssre  12549  supicc  12550  supiccub  12551  supicclub  12552  icccld  22791  iccntr  22845  icccmplem2  22847  icccmplem3  22848  icccmp  22849  retopconn  22853  iccconn  22854  cnmpt2pc  22948  iihalf1cn  22952  iihalf2cn  22954  icoopnst  22959  iocopnst  22960  icchmeo  22961  xrhmeo  22966  icccvx  22970  cnheiborlem  22974  htpycc  23000  pcocn  23037  pcohtpylem  23039  pcopt  23042  pcopt2  23043  pcoass  23044  pcorevlem  23046  ivthlem2  23443  ivthlem3  23444  ivthicc  23449  evthicc  23450  ovolficcss  23460  ovolicc1  23507  ovolicc2  23513  ovolicc  23514  iccmbl  23557  ovolioo  23559  dyadss  23585  volcn  23597  volivth  23598  vitalilem2  23600  vitalilem4  23602  mbfimaicc  23622  mbfi1fseqlem4  23709  itgioo  23806  rollelem  23976  rolle  23977  cmvth  23978  mvth  23979  dvlip  23980  c1liplem1  23983  c1lip1  23984  c1lip3  23986  dvgt0lem1  23989  dvgt0lem2  23990  dvgt0  23991  dvlt0  23992  dvge0  23993  dvle  23994  dvivthlem1  23995  dvivth  23997  dvne0  23998  lhop1lem  24000  dvcvx  24007  dvfsumle  24008  dvfsumge  24009  dvfsumabs  24010  ftc1lem1  24022  ftc1a  24024  ftc1lem4  24026  ftc1lem5  24027  ftc1lem6  24028  ftc1  24029  ftc1cn  24030  ftc2  24031  ftc2ditglem  24032  ftc2ditg  24033  itgparts  24034  itgsubstlem  24035  aalioulem3  24313  reeff1olem  24424  efcvx  24427  pilem3  24431  pilem3OLD  24432  pige3  24494  sinord  24505  recosf1o  24506  resinf1o  24507  efif1olem4  24516  asinrecl  24853  acosrecl  24854  emre  24956  pntlem3  25522  ttgcontlem1  25989  signsply0  30963  iblidicc  31005  ftc2re  31011  iccsconn  31562  iccllysconn  31564  cvmliftlem10  31608  ivthALT  32660  sin2h  33718  cos2h  33719  mblfinlem2  33766  ftc1cnnclem  33801  ftc1cnnc  33802  ftc1anclem7  33809  ftc1anc  33811  ftc2nc  33812  areacirclem2  33819  areacirclem3  33820  areacirclem4  33821  areacirc  33823  iccbnd  33956  icccmpALT  33957  itgpowd  38305  arearect  38306  areaquad  38307  lhe4.4ex1a  39033  lefldiveq  39992  iccssred  40216  itgsin0pilem1  40650  ibliccsinexp  40651  iblioosinexp  40653  itgsinexplem1  40654  itgsinexp  40655  iblspltprt  40673  fourierdlem5  40813  fourierdlem9  40817  fourierdlem18  40826  fourierdlem24  40832  fourierdlem62  40869  fourierdlem66  40873  fourierdlem74  40881  fourierdlem75  40882  fourierdlem83  40890  fourierdlem87  40894  fourierdlem93  40900  fourierdlem95  40902  fourierdlem102  40909  fourierdlem103  40910  fourierdlem104  40911  fourierdlem112  40919  fourierdlem114  40921  sqwvfoura  40929  sqwvfourb  40930
  Copyright terms: Public domain W3C validator