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

Theorem iccssre 11609
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 11592 . . . . 5  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( x  e.  ( A [,] B )  <-> 
( x  e.  RR  /\  A  <_  x  /\  x  <_  B ) ) )
21biimp3a 1326 . . . 4  |-  ( ( A  e.  RR  /\  B  e.  RR  /\  x  e.  ( A [,] B
) )  ->  (
x  e.  RR  /\  A  <_  x  /\  x  <_  B ) )
32simp1d 1006 . . 3  |-  ( ( A  e.  RR  /\  B  e.  RR  /\  x  e.  ( A [,] B
) )  ->  x  e.  RR )
433expia 1196 . 2  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( x  e.  ( A [,] B )  ->  x  e.  RR ) )
54ssrdv 3495 1  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A [,] B
)  C_  RR )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    /\ w3a 971    e. wcel 1823    C_ wss 3461   class class class wbr 4439  (class class class)co 6270   RRcr 9480    <_ cle 9618   [,]cicc 11535
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-8 1825  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-sep 4560  ax-nul 4568  ax-pow 4615  ax-pr 4676  ax-un 6565  ax-cnex 9537  ax-resscn 9538  ax-pre-lttri 9555  ax-pre-lttrn 9556
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-mo 2289  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-nel 2652  df-ral 2809  df-rex 2810  df-rab 2813  df-v 3108  df-sbc 3325  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-pw 4001  df-sn 4017  df-pr 4019  df-op 4023  df-uni 4236  df-br 4440  df-opab 4498  df-mpt 4499  df-id 4784  df-po 4789  df-so 4790  df-xp 4994  df-rel 4995  df-cnv 4996  df-co 4997  df-dm 4998  df-rn 4999  df-res 5000  df-ima 5001  df-iota 5534  df-fun 5572  df-fn 5573  df-f 5574  df-f1 5575  df-fo 5576  df-f1o 5577  df-fv 5578  df-ov 6273  df-oprab 6274  df-mpt2 6275  df-er 7303  df-en 7510  df-dom 7511  df-sdom 7512  df-pnf 9619  df-mnf 9620  df-xr 9621  df-ltxr 9622  df-le 9623  df-icc 11539
This theorem is referenced by:  iccsupr  11620  iccsplit  11656  iccshftri  11658  iccshftli  11660  iccdili  11662  icccntri  11664  unitssre  11670  supicc  11671  supiccub  11672  supicclub  11673  icccld  21440  iccntr  21492  icccmplem2  21494  icccmplem3  21495  icccmp  21496  retopcon  21500  iccconn  21501  cnmpt2pc  21594  iihalf1cn  21598  iihalf2cn  21600  icoopnst  21605  iocopnst  21606  icchmeo  21607  xrhmeo  21612  icccvx  21616  cnheiborlem  21620  htpycc  21646  pcocn  21683  pcohtpylem  21685  pcopt  21688  pcopt2  21689  pcoass  21690  pcorevlem  21692  ivthlem2  22030  ivthlem3  22031  ivthicc  22036  evthicc  22037  ovolficcss  22047  ovolicc1  22093  ovolicc2  22099  ovolicc  22100  iccmbl  22142  ovolioo  22144  dyadss  22169  volcn  22181  volivth  22182  vitalilem2  22184  vitalilem4  22186  mbfimaicc  22206  mbfi1fseqlem4  22291  itgioo  22388  rollelem  22556  rolle  22557  cmvth  22558  mvth  22559  dvlip  22560  c1liplem1  22563  c1lip1  22564  c1lip3  22566  dvgt0lem1  22569  dvgt0lem2  22570  dvgt0  22571  dvlt0  22572  dvge0  22573  dvle  22574  dvivthlem1  22575  dvivth  22577  dvne0  22578  lhop1lem  22580  dvcvx  22587  dvfsumle  22588  dvfsumge  22589  dvfsumabs  22590  ftc1lem1  22602  ftc1a  22604  ftc1lem4  22606  ftc1lem5  22607  ftc1lem6  22608  ftc1  22609  ftc1cn  22610  ftc2  22611  ftc2ditglem  22612  ftc2ditg  22613  itgparts  22614  itgsubstlem  22615  aalioulem3  22896  reeff1olem  23007  efcvx  23010  pilem3  23014  pige3  23076  sinord  23087  recosf1o  23088  resinf1o  23089  efif1olem4  23098  asinrecl  23430  acosrecl  23431  emre  23533  pntlem3  23992  ttgcontlem1  24390  signsply0  28772  iccscon  28957  iccllyscon  28959  cvmliftlem10  29003  sin2h  30285  cos2h  30286  mblfinlem2  30292  ftc1cnnclem  30328  ftc1cnnc  30329  ftc1anclem7  30336  ftc1anc  30338  ftc2nc  30339  areacirclem2  30348  areacirclem3  30349  areacirclem4  30350  areacirc  30352  ivthALT  30393  iccbnd  30576  icccmpALT  30577  itgpowd  31423  arearect  31424  areaquad  31425  lhe4.4ex1a  31475  lefldiveq  31722  iccssred  31778  itgsin0pilem1  31987  ibliccsinexp  31988  iblioosinexp  31990  itgsinexplem1  31991  itgsinexp  31992  iblspltprt  32011  fourierdlem5  32133  fourierdlem9  32137  fourierdlem18  32146  fourierdlem24  32152  fourierdlem62  32190  fourierdlem66  32194  fourierdlem74  32202  fourierdlem75  32203  fourierdlem83  32211  fourierdlem87  32215  fourierdlem93  32221  fourierdlem95  32223  fourierdlem102  32230  fourierdlem103  32231  fourierdlem104  32232  fourierdlem112  32240  fourierdlem114  32242  sqwvfoura  32250  sqwvfourb  32251
  Copyright terms: Public domain W3C validator