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

Theorem iccssre 12240
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 12223 . . . . 5 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑥 ∈ (𝐴[,]𝐵) ↔ (𝑥 ∈ ℝ ∧ 𝐴𝑥𝑥𝐵)))
21biimp3a 1430 . . . 4 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝑥 ∈ ℝ ∧ 𝐴𝑥𝑥𝐵))
32simp1d 1071 . . 3 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ∈ ℝ)
433expia 1265 . 2 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑥 ∈ (𝐴[,]𝐵) → 𝑥 ∈ ℝ))
54ssrdv 3601 1 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1036  wcel 1988  wss 3567   class class class wbr 4644  (class class class)co 6635  cr 9920  cle 10060  [,]cicc 12163
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-8 1990  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-sep 4772  ax-nul 4780  ax-pow 4834  ax-pr 4897  ax-un 6934  ax-cnex 9977  ax-resscn 9978  ax-pre-lttri 9995  ax-pre-lttrn 9996
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ne 2792  df-nel 2895  df-ral 2914  df-rex 2915  df-rab 2918  df-v 3197  df-sbc 3430  df-csb 3527  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-if 4078  df-pw 4151  df-sn 4169  df-pr 4171  df-op 4175  df-uni 4428  df-br 4645  df-opab 4704  df-mpt 4721  df-id 5014  df-po 5025  df-so 5026  df-xp 5110  df-rel 5111  df-cnv 5112  df-co 5113  df-dm 5114  df-rn 5115  df-res 5116  df-ima 5117  df-iota 5839  df-fun 5878  df-fn 5879  df-f 5880  df-f1 5881  df-fo 5882  df-f1o 5883  df-fv 5884  df-ov 6638  df-oprab 6639  df-mpt2 6640  df-er 7727  df-en 7941  df-dom 7942  df-sdom 7943  df-pnf 10061  df-mnf 10062  df-xr 10063  df-ltxr 10064  df-le 10065  df-icc 12167
This theorem is referenced by:  iccsupr  12251  iccsplit  12290  iccshftri  12292  iccshftli  12294  iccdili  12296  icccntri  12298  unitssre  12304  supicc  12305  supiccub  12306  supicclub  12307  icccld  22551  iccntr  22605  icccmplem2  22607  icccmplem3  22608  icccmp  22609  retopconn  22613  iccconn  22614  cnmpt2pc  22708  iihalf1cn  22712  iihalf2cn  22714  icoopnst  22719  iocopnst  22720  icchmeo  22721  xrhmeo  22726  icccvx  22730  cnheiborlem  22734  htpycc  22760  pcocn  22798  pcohtpylem  22800  pcopt  22803  pcopt2  22804  pcoass  22805  pcorevlem  22807  ivthlem2  23202  ivthlem3  23203  ivthicc  23208  evthicc  23209  ovolficcss  23219  ovolicc1  23265  ovolicc2  23271  ovolicc  23272  iccmbl  23315  ovolioo  23317  dyadss  23343  volcn  23355  volivth  23356  vitalilem2  23359  vitalilem4  23361  mbfimaicc  23381  mbfi1fseqlem4  23466  itgioo  23563  rollelem  23733  rolle  23734  cmvth  23735  mvth  23736  dvlip  23737  c1liplem1  23740  c1lip1  23741  c1lip3  23743  dvgt0lem1  23746  dvgt0lem2  23747  dvgt0  23748  dvlt0  23749  dvge0  23750  dvle  23751  dvivthlem1  23752  dvivth  23754  dvne0  23755  lhop1lem  23757  dvcvx  23764  dvfsumle  23765  dvfsumge  23766  dvfsumabs  23767  ftc1lem1  23779  ftc1a  23781  ftc1lem4  23783  ftc1lem5  23784  ftc1lem6  23785  ftc1  23786  ftc1cn  23787  ftc2  23788  ftc2ditglem  23789  ftc2ditg  23790  itgparts  23791  itgsubstlem  23792  aalioulem3  24070  reeff1olem  24181  efcvx  24184  pilem3  24188  pige3  24250  sinord  24261  recosf1o  24262  resinf1o  24263  efif1olem4  24272  asinrecl  24610  acosrecl  24611  emre  24713  pntlem3  25279  ttgcontlem1  25746  signsply0  30602  iblidicc  30644  ftc2re  30650  iccsconn  31204  iccllysconn  31206  cvmliftlem10  31250  ivthALT  32305  sin2h  33370  cos2h  33371  mblfinlem2  33418  ftc1cnnclem  33454  ftc1cnnc  33455  ftc1anclem7  33462  ftc1anc  33464  ftc2nc  33465  areacirclem2  33472  areacirclem3  33473  areacirclem4  33474  areacirc  33476  iccbnd  33610  icccmpALT  33611  itgpowd  37619  arearect  37620  areaquad  37621  lhe4.4ex1a  38348  lefldiveq  39318  iccssred  39530  itgsin0pilem1  39928  ibliccsinexp  39929  iblioosinexp  39931  itgsinexplem1  39932  itgsinexp  39933  iblspltprt  39952  fourierdlem5  40092  fourierdlem9  40096  fourierdlem18  40105  fourierdlem24  40111  fourierdlem62  40148  fourierdlem66  40152  fourierdlem74  40160  fourierdlem75  40161  fourierdlem83  40169  fourierdlem87  40173  fourierdlem93  40179  fourierdlem95  40181  fourierdlem102  40188  fourierdlem103  40189  fourierdlem104  40190  fourierdlem112  40198  fourierdlem114  40200  sqwvfoura  40208  sqwvfourb  40209
  Copyright terms: Public domain W3C validator