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

Theorem iccssre 12797
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 12780 . . . . 5 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑥 ∈ (𝐴[,]𝐵) ↔ (𝑥 ∈ ℝ ∧ 𝐴𝑥𝑥𝐵)))
21biimp3a 1466 . . . 4 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝑥 ∈ ℝ ∧ 𝐴𝑥𝑥𝐵))
32simp1d 1139 . . 3 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ∈ ℝ)
433expia 1118 . 2 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑥 ∈ (𝐴[,]𝐵) → 𝑥 ∈ ℝ))
54ssrdv 3949 1 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  w3a 1084  wcel 2115  wss 3910   class class class wbr 5039  (class class class)co 7130  cr 10513  cle 10653  [,]cicc 12719
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 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2178  ax-ext 2793  ax-sep 5176  ax-nul 5183  ax-pow 5239  ax-pr 5303  ax-un 7436  ax-cnex 10570  ax-resscn 10571  ax-pre-lttri 10588  ax-pre-lttrn 10589
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 2071  df-mo 2623  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2892  df-nfc 2960  df-ne 3008  df-nel 3112  df-ral 3131  df-rex 3132  df-rab 3135  df-v 3473  df-sbc 3750  df-csb 3858  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4267  df-if 4441  df-pw 4514  df-sn 4541  df-pr 4543  df-op 4547  df-uni 4812  df-br 5040  df-opab 5102  df-mpt 5120  df-id 5433  df-po 5447  df-so 5448  df-xp 5534  df-rel 5535  df-cnv 5536  df-co 5537  df-dm 5538  df-rn 5539  df-res 5540  df-ima 5541  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-ov 7133  df-oprab 7134  df-mpo 7135  df-er 8264  df-en 8485  df-dom 8486  df-sdom 8487  df-pnf 10654  df-mnf 10655  df-xr 10656  df-ltxr 10657  df-le 10658  df-icc 12723
This theorem is referenced by:  iccssred  12802  iccsupr  12810  iccsplit  12853  iccshftri  12855  iccshftli  12857  iccdili  12859  icccntri  12861  unitssre  12867  supicc  12869  supiccub  12870  supicclub  12871  icccld  23351  iccntr  23405  icccmplem2  23407  icccmplem3  23408  icccmp  23409  retopconn  23413  iccconn  23414  cnmpopc  23512  iihalf1cn  23516  iihalf2cn  23518  icoopnst  23523  iocopnst  23524  icchmeo  23525  xrhmeo  23530  icccvx  23534  cnheiborlem  23538  htpycc  23564  pcocn  23601  pcohtpylem  23603  pcopt  23606  pcopt2  23607  pcoass  23608  pcorevlem  23610  ivthlem2  24035  ivthlem3  24036  ivthicc  24041  evthicc  24042  ovolficcss  24052  ovolicc1  24099  ovolicc2  24105  ovolicc  24106  iccmbl  24149  ovolioo  24151  dyadss  24177  volcn  24189  volivth  24190  vitalilem2  24192  vitalilem4  24194  mbfimaicc  24214  mbfi1fseqlem4  24301  itgioo  24398  rollelem  24571  rolle  24572  cmvth  24573  mvth  24574  dvlip  24575  c1liplem1  24578  c1lip1  24579  c1lip3  24581  dvgt0lem1  24584  dvgt0lem2  24585  dvgt0  24586  dvlt0  24587  dvge0  24588  dvle  24589  dvivthlem1  24590  dvivth  24592  dvne0  24593  lhop1lem  24595  dvcvx  24602  dvfsumle  24603  dvfsumge  24604  dvfsumabs  24605  ftc1lem1  24617  ftc1a  24619  ftc1lem4  24621  ftc1lem5  24622  ftc1lem6  24623  ftc1  24624  ftc1cn  24625  ftc2  24626  ftc2ditglem  24627  ftc2ditg  24628  itgparts  24629  itgsubstlem  24630  itgpowd  24632  aalioulem3  24909  reeff1olem  25020  efcvx  25023  pilem3  25027  pige3ALT  25091  sinord  25105  recosf1o  25106  resinf1o  25107  efif1olem4  25116  asinrecl  25467  acosrecl  25468  emre  25570  pntlem3  26172  ttgcontlem1  26658  signsply0  31829  iblidicc  31871  ftc2re  31877  iccsconn  32503  iccllysconn  32505  cvmliftlem10  32549  ivthALT  33691  sin2h  34929  cos2h  34930  mblfinlem2  34977  ftc1cnnclem  35010  ftc1cnnc  35011  ftc1anclem7  35018  ftc1anc  35020  ftc2nc  35021  areacirclem2  35028  areacirclem3  35029  areacirclem4  35030  areacirc  35032  iccbnd  35160  icccmpALT  35161  arearect  39972  areaquad  39973  lhe4.4ex1a  40844  lefldiveq  41741  itgsin0pilem1  42411  ibliccsinexp  42412  iblioosinexp  42414  itgsinexplem1  42415  itgsinexp  42416  iblspltprt  42434  fourierdlem5  42573  fourierdlem9  42577  fourierdlem18  42586  fourierdlem24  42592  fourierdlem62  42629  fourierdlem66  42633  fourierdlem74  42641  fourierdlem75  42642  fourierdlem83  42650  fourierdlem87  42654  fourierdlem93  42660  fourierdlem95  42662  fourierdlem102  42669  fourierdlem103  42670  fourierdlem104  42671  fourierdlem112  42679  fourierdlem114  42681  sqwvfoura  42689  sqwvfourb  42690
  Copyright terms: Public domain W3C validator