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

Theorem iccssxr 13439
Description: A closed interval is a set of extended reals. (Contributed by FL, 28-Jul-2008.) (Revised by Mario Carneiro, 4-Jul-2014.)
Assertion
Ref Expression
iccssxr (𝐴[,]𝐵) ⊆ ℝ*

Proof of Theorem iccssxr
Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-icc 13363 . 2 [,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑧𝑧𝑦)})
21ixxssxr 13368 1 (𝐴[,]𝐵) ⊆ ℝ*
Colors of variables: wff setvar class
Syntax hints:  wss 3945  (class class class)co 7417  *cxr 11277  cle 11279  [,]cicc 13359
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-sep 5299  ax-nul 5306  ax-pr 5428  ax-un 7739  ax-cnex 11194  ax-resscn 11195
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2931  df-ral 3052  df-rex 3061  df-rab 3420  df-v 3465  df-sbc 3775  df-csb 3891  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4909  df-iun 4998  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5575  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-iota 6499  df-fun 6549  df-fn 6550  df-f 6551  df-fv 6555  df-ov 7420  df-oprab 7421  df-mpo 7422  df-1st 7992  df-2nd 7993  df-xr 11282  df-icc 13363
This theorem is referenced by:  eliccxr  13444  supicclub2  13513  lecldbas  23153  ordtresticc  23157  prdsxmetlem  24304  xrge0gsumle  24779  xrge0tsms  24780  metdscn  24802  iccpnfhmeo  24900  xrhmeo  24901  volsup  25515  volsup2  25564  volivth  25566  itg2le  25699  itg2const2  25701  itg2lea  25704  itg2eqa  25705  itg2split  25709  itg2gt0  25720  dvgt0lem1  25965  radcnvlt1  26384  radcnvle  26386  pserulm  26388  psercnlem2  26391  psercnlem1  26392  psercn  26393  pserdvlem1  26394  pserdvlem2  26395  abelthlem3  26400  abelth  26408  logtayl  26624  xrge0infss  32587  xrge0infssd  32588  xrge0subcld  32590  infxrge0lb  32591  infxrge0glb  32592  infxrge0gelb  32593  xrge0base  32798  xrge00  32799  xrge0mulgnn0  32802  xrge0addass  32803  xrge0addgt0  32804  xrge0adddir  32805  xrge0adddi  32806  xrge0npcan  32807  xrge0tsmsd  32828  xrge0slmod  33120  xrge0iifiso  33606  xrge0iifhmeo  33607  xrge0pluscn  33611  xrge0mulc1cn  33612  xrge0tmdALT  33617  lmlimxrge0  33619  pnfneige0  33622  lmxrge0  33623  esummono  33743  esumpad  33744  esumpad2  33745  esumle  33747  gsumesum  33748  esumlub  33749  esumlef  33751  esumcst  33752  esumrnmpt2  33757  esumfsup  33759  esumpinfval  33762  esumpfinvallem  33763  esumpinfsum  33766  esumpmono  33768  esummulc2  33771  esumdivc  33772  hasheuni  33774  esumcvg  33775  esumgect  33779  esum2d  33782  measun  33900  measunl  33905  measiun  33907  voliune  33918  volfiniune  33919  ddemeas  33925  omsfval  33984  omsf  33986  oms0  33987  omssubaddlem  33989  omssubadd  33990  baselcarsg  33996  0elcarsg  33997  difelcarsg  34000  inelcarsg  34001  carsgsigalem  34005  carsggect  34008  carsgclctunlem2  34009  carsgclctunlem3  34010  carsgclctun  34011  omsmeas  34013  pmeasmono  34014  probmeasb  34120  itg2addnclem  37214  ftc1anc  37244  xadd0ge  44765  xrge0nemnfd  44777  xadd0ge2  44786  ge0lere  44980  inficc  44982  iccdificc  44987  fourierdlem1  45559  fourierdlem20  45578  fourierdlem27  45585  fourierdlem87  45644  fge0iccico  45821  gsumge0cl  45822  sge0sn  45830  sge0tsms  45831  sge0xrcl  45836  sge0pr  45845  sge0prle  45852  sge0le  45858  sge0split  45860  sge0p1  45865  sge0rernmpt  45873  sge0xrclmpt  45879  sge0xadd  45886  meaxrcl  45912  meadjun  45913  voliunsge0lem  45923  caragen0  45957  omexrcl  45958  caragenunidm  45959  caragendifcl  45965  omeunle  45967  omeiunle  45968  carageniuncl  45974  ovn0lem  46016  ovnxrcl  46020  hoidmvlelem3  46048  hoidmvlelem4  46049  vonxrcl  46119  icccldii  48049
  Copyright terms: Public domain W3C validator