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

Theorem iccssre 11716
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 11699 . . . . 5  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( x  e.  ( A [,] B )  <-> 
( x  e.  RR  /\  A  <_  x  /\  x  <_  B ) ) )
21biimp3a 1364 . . . 4  |-  ( ( A  e.  RR  /\  B  e.  RR  /\  x  e.  ( A [,] B
) )  ->  (
x  e.  RR  /\  A  <_  x  /\  x  <_  B ) )
32simp1d 1017 . . 3  |-  ( ( A  e.  RR  /\  B  e.  RR  /\  x  e.  ( A [,] B
) )  ->  x  e.  RR )
433expia 1207 . 2  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( x  e.  ( A [,] B )  ->  x  e.  RR ) )
54ssrdv 3470 1  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A [,] B
)  C_  RR )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    /\ w3a 982    e. wcel 1868    C_ wss 3436   class class class wbr 4420  (class class class)co 6301   RRcr 9538    <_ cle 9676   [,]cicc 11638
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-8 1870  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-sep 4543  ax-nul 4551  ax-pow 4598  ax-pr 4656  ax-un 6593  ax-cnex 9595  ax-resscn 9596  ax-pre-lttri 9613  ax-pre-lttrn 9614
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-nel 2621  df-ral 2780  df-rex 2781  df-rab 2784  df-v 3083  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3910  df-pw 3981  df-sn 3997  df-pr 3999  df-op 4003  df-uni 4217  df-br 4421  df-opab 4480  df-mpt 4481  df-id 4764  df-po 4770  df-so 4771  df-xp 4855  df-rel 4856  df-cnv 4857  df-co 4858  df-dm 4859  df-rn 4860  df-res 4861  df-ima 4862  df-iota 5561  df-fun 5599  df-fn 5600  df-f 5601  df-f1 5602  df-fo 5603  df-f1o 5604  df-fv 5605  df-ov 6304  df-oprab 6305  df-mpt2 6306  df-er 7367  df-en 7574  df-dom 7575  df-sdom 7576  df-pnf 9677  df-mnf 9678  df-xr 9679  df-ltxr 9680  df-le 9681  df-icc 11642
This theorem is referenced by:  iccsupr  11727  iccsplit  11765  iccshftri  11767  iccshftli  11769  iccdili  11771  icccntri  11773  unitssre  11779  supicc  11780  supiccub  11781  supicclub  11782  icccld  21771  iccntr  21823  icccmplem2  21825  icccmplem3  21826  icccmp  21827  retopcon  21831  iccconn  21832  cnmpt2pc  21940  iihalf1cn  21944  iihalf2cn  21946  icoopnst  21951  iocopnst  21952  icchmeo  21953  xrhmeo  21958  icccvx  21962  cnheiborlem  21966  htpycc  21995  pcocn  22032  pcohtpylem  22034  pcopt  22037  pcopt2  22038  pcoass  22039  pcorevlem  22041  ivthlem2  22387  ivthlem3  22388  ivthicc  22393  evthicc  22394  ovolficcss  22406  ovolicc1  22453  ovolicc2  22460  ovolicc  22461  iccmbl  22503  ovolioo  22505  dyadss  22536  volcn  22548  volivth  22549  vitalilem2  22551  vitalilem4  22553  mbfimaicc  22573  mbfi1fseqlem4  22660  itgioo  22757  rollelem  22925  rolle  22926  cmvth  22927  mvth  22928  dvlip  22929  c1liplem1  22932  c1lip1  22933  c1lip3  22935  dvgt0lem1  22938  dvgt0lem2  22939  dvgt0  22940  dvlt0  22941  dvge0  22942  dvle  22943  dvivthlem1  22944  dvivth  22946  dvne0  22947  lhop1lem  22949  dvcvx  22956  dvfsumle  22957  dvfsumge  22958  dvfsumabs  22959  ftc1lem1  22971  ftc1a  22973  ftc1lem4  22975  ftc1lem5  22976  ftc1lem6  22977  ftc1  22978  ftc1cn  22979  ftc2  22980  ftc2ditglem  22981  ftc2ditg  22982  itgparts  22983  itgsubstlem  22984  aalioulem3  23274  reeff1olem  23385  efcvx  23388  pilem3  23393  pilem3OLD  23394  pige3  23456  sinord  23467  recosf1o  23468  resinf1o  23469  efif1olem4  23478  asinrecl  23812  acosrecl  23813  emre  23915  pntlem3  24431  ttgcontlem1  24899  signsply0  29433  iccscon  29964  iccllyscon  29966  cvmliftlem10  30010  ivthALT  30981  sin2h  31846  cos2h  31847  mblfinlem2  31889  ftc1cnnclem  31926  ftc1cnnc  31927  ftc1anclem7  31934  ftc1anc  31936  ftc2nc  31937  areacirclem2  31944  areacirclem3  31945  areacirclem4  31946  areacirc  31948  iccbnd  32083  icccmpALT  32084  itgpowd  36016  arearect  36017  areaquad  36018  lhe4.4ex1a  36533  lefldiveq  37345  iccssred  37430  itgsin0pilem1  37643  ibliccsinexp  37644  iblioosinexp  37646  itgsinexplem1  37647  itgsinexp  37648  iblspltprt  37667  fourierdlem5  37791  fourierdlem9  37795  fourierdlem18  37804  fourierdlem24  37810  fourierdlem62  37849  fourierdlem66  37853  fourierdlem74  37861  fourierdlem75  37862  fourierdlem83  37870  fourierdlem87  37874  fourierdlem93  37880  fourierdlem95  37882  fourierdlem102  37889  fourierdlem103  37890  fourierdlem104  37891  fourierdlem112  37899  fourierdlem114  37901  sqwvfoura  37909  sqwvfourb  37910
  Copyright terms: Public domain W3C validator