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

Theorem iblmbf 22152
 Description: An integrable function is measurable. (Contributed by Mario Carneiro, 7-Jul-2014.)
Assertion
Ref Expression
iblmbf MblFn

Proof of Theorem iblmbf
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-ibl 22009 . . 3 MblFn
2 ssrab2 3570 . . 3 MblFn MblFn
31, 2eqsstri 3519 . 2 MblFn
43sseli 3485 1 MblFn
 Colors of variables: wff setvar class Syntax hints:   wi 4   wa 369   wcel 1804  wral 2793  crab 2797  csb 3420  cif 3926   class class class wbr 4437   cmpt 4495   cdm 4989  cfv 5578  (class class class)co 6281  cr 9494  cc0 9495  ci 9497   cle 9632   cdiv 10213  c3 10593  cfz 11683  cexp 12148  cre 12912  MblFncmbf 22001  citg2 22003  cibl 22004 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-rab 2802  df-in 3468  df-ss 3475  df-ibl 22009 This theorem is referenced by:  iblcnlem  22173  itgcnlem  22174  itgcnval  22184  itgre  22185  itgim  22186  iblneg  22187  itgneg  22188  iblss  22189  iblss2  22190  itgge0  22195  itgss3  22199  itgless  22201  iblsub  22206  itgadd  22209  itgsub  22210  itgfsum  22211  iblabs  22213  iblmulc2  22215  itgmulc2  22218  itgabs  22219  itgsplit  22220  bddmulibl  22223  itggt0  22226  itgcn  22227  ditgswap  22241  ditgsplitlem  22242  ftc1a  22416  itgsubstlem  22427  iblulm  22780  itgulm  22781  ibladdnc  30048  itgaddnclem1  30049  itgaddnclem2  30050  itgaddnc  30051  iblsubnc  30052  itgsubnc  30053  iblabsnclem  30054  iblabsnc  30055  iblmulc2nc  30056  itgmulc2nclem2  30058  itgmulc2nc  30059  itgabsnc  30060  ftc1cnnclem  30064  ftc1anclem2  30067  ftc1anclem4  30069  ftc1anclem5  30070  ftc1anclem6  30071  ftc1anclem8  30073
 Copyright terms: Public domain W3C validator