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

Theorem iccssre 11606
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  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A [,] B
)  C_  RR )

Proof of Theorem iccssre
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 elicc2 11589 . . . . 5  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( x  e.  ( A [,] B )  <-> 
( x  e.  RR  /\  A  <_  x  /\  x  <_  B ) ) )
21biimp3a 1328 . . . 4  |-  ( ( A  e.  RR  /\  B  e.  RR  /\  x  e.  ( A [,] B
) )  ->  (
x  e.  RR  /\  A  <_  x  /\  x  <_  B ) )
32simp1d 1008 . . 3  |-  ( ( A  e.  RR  /\  B  e.  RR  /\  x  e.  ( A [,] B
) )  ->  x  e.  RR )
433expia 1198 . 2  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( x  e.  ( A [,] B )  ->  x  e.  RR ) )
54ssrdv 3510 1  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A [,] B
)  C_  RR )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 973    e. wcel 1767    C_ wss 3476   class class class wbr 4447  (class class class)co 6284   RRcr 9491    <_ cle 9629   [,]cicc 11532
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568  ax-nul 4576  ax-pow 4625  ax-pr 4686  ax-un 6576  ax-cnex 9548  ax-resscn 9549  ax-pre-lttri 9566  ax-pre-lttrn 9567
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-nel 2665  df-ral 2819  df-rex 2820  df-rab 2823  df-v 3115  df-sbc 3332  df-csb 3436  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-pw 4012  df-sn 4028  df-pr 4030  df-op 4034  df-uni 4246  df-br 4448  df-opab 4506  df-mpt 4507  df-id 4795  df-po 4800  df-so 4801  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012  df-iota 5551  df-fun 5590  df-fn 5591  df-f 5592  df-f1 5593  df-fo 5594  df-f1o 5595  df-fv 5596  df-ov 6287  df-oprab 6288  df-mpt2 6289  df-er 7311  df-en 7517  df-dom 7518  df-sdom 7519  df-pnf 9630  df-mnf 9631  df-xr 9632  df-ltxr 9633  df-le 9634  df-icc 11536
This theorem is referenced by:  iccsupr  11617  iccsplit  11653  iccshftri  11655  iccshftli  11657  iccdili  11659  icccntri  11661  unitssre  11667  supicc  11668  supiccub  11669  supicclub  11670  icccld  21037  iccntr  21089  icccmplem2  21091  icccmplem3  21092  icccmp  21093  retopcon  21097  iccconn  21098  cnmpt2pc  21191  iihalf1cn  21195  iihalf2cn  21197  icoopnst  21202  iocopnst  21203  icchmeo  21204  xrhmeo  21209  icccvx  21213  cnheiborlem  21217  htpycc  21243  pcocn  21280  pcohtpylem  21282  pcopt  21285  pcopt2  21286  pcoass  21287  pcorevlem  21289  ivthlem2  21627  ivthlem3  21628  ivthicc  21633  evthicc  21634  ovolficcss  21644  ovolicc1  21690  ovolicc2  21696  ovolicc  21697  iccmbl  21739  ovolioo  21741  dyadss  21766  volcn  21778  volivth  21779  vitalilem2  21781  vitalilem4  21783  mbfimaicc  21803  mbfi1fseqlem4  21888  itgioo  21985  rollelem  22153  rolle  22154  cmvth  22155  mvth  22156  dvlip  22157  c1liplem1  22160  c1lip1  22161  c1lip3  22163  dvgt0lem1  22166  dvgt0lem2  22167  dvgt0  22168  dvlt0  22169  dvge0  22170  dvle  22171  dvivthlem1  22172  dvivth  22174  dvne0  22175  lhop1lem  22177  dvcvx  22184  dvfsumle  22185  dvfsumge  22186  dvfsumabs  22187  ftc1lem1  22199  ftc1a  22201  ftc1lem4  22203  ftc1lem5  22204  ftc1lem6  22205  ftc1  22206  ftc1cn  22207  ftc2  22208  ftc2ditglem  22209  ftc2ditg  22210  itgparts  22211  itgsubstlem  22212  aalioulem3  22492  reeff1olem  22603  efcvx  22606  pilem3  22610  pige3  22671  sinord  22682  recosf1o  22683  resinf1o  22684  efif1olem4  22693  asinrecl  22989  acosrecl  22990  emre  23091  pntlem3  23550  ttgcontlem1  23892  signsply0  28176  iccscon  28361  iccllyscon  28363  cvmliftlem10  28407  sin2h  29650  cos2h  29651  mblfinlem2  29657  ftc1cnnclem  29693  ftc1cnnc  29694  ftc1anclem7  29701  ftc1anc  29703  ftc2nc  29704  areacirclem2  29713  areacirclem3  29714  areacirclem4  29715  areacirc  29717  ivthALT  29758  iccbnd  29967  icccmpALT  29968  itgpowd  30815  arearect  30816  areaquad  30817  lhe4.4ex1a  30862  lefldiveq  31087  iccssred  31131  iccshift  31150  limciccioolb  31191  limcicciooub  31207  icccncfext  31254  cncfiooicclem1  31260  itgsin0pilem1  31295  ibliccsinexp  31296  iblioosinexp  31298  itgsinexplem1  31299  itgsinexp  31300  ibliooicc  31317  iblspltprt  31319  itgsubsticclem  31321  itgiccshift  31326  itgperiod  31327  itgsbtaddcnst  31328  fourierdlem5  31440  fourierdlem9  31444  fourierdlem18  31453  fourierdlem24  31459  fourierdlem40  31475  fourierdlem62  31497  fourierdlem66  31501  fourierdlem74  31509  fourierdlem75  31510  fourierdlem76  31511  fourierdlem78  31513  fourierdlem81  31516  fourierdlem83  31518  fourierdlem87  31522  fourierdlem93  31528  fourierdlem95  31530  fourierdlem102  31537  fourierdlem103  31538  fourierdlem104  31539  fourierdlem112  31547  fourierdlem114  31549  sqwvfoura  31557  sqwvfourb  31558
  Copyright terms: Public domain W3C validator