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

Theorem isibl 21361
 Description: The predicate " is integrable". The "integrable" predicate corresponds roughly to the range of validity of , which is to say that the expression doesn't make sense unless . (Contributed by Mario Carneiro, 28-Jun-2014.) (Revised by Mario Carneiro, 23-Aug-2014.)
Hypotheses
Ref Expression
isibl.1
isibl.2
isibl.3
isibl.4
Assertion
Ref Expression
isibl MblFn
Distinct variable groups:   ,,   ,   ,,   ,,
Allowed substitution hints:   ()   (,)   (,)

Proof of Theorem isibl
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fvex 5801 . . . . . . . . 9
2 nfcv 2613 . . . . . . . . 9
3 breq2 4396 . . . . . . . . . . 11
43anbi2d 703 . . . . . . . . . 10
5 id 22 . . . . . . . . . 10
64, 5ifbieq1d 3912 . . . . . . . . 9
71, 2, 6csbief 3413 . . . . . . . 8
8 dmeq 5140 . . . . . . . . . . 11
98eleq2d 2521 . . . . . . . . . 10
10 fveq1 5790 . . . . . . . . . . . . 13
1110oveq1d 6207 . . . . . . . . . . . 12
1211fveq2d 5795 . . . . . . . . . . 11
1312breq2d 4404 . . . . . . . . . 10
149, 13anbi12d 710 . . . . . . . . 9
1514, 12ifbieq1d 3912 . . . . . . . 8
167, 15syl5eq 2504 . . . . . . 7
1716mpteq2dv 4479 . . . . . 6
1817fveq2d 5795 . . . . 5
1918eleq1d 2520 . . . 4
2019ralbidv 2838 . . 3
21 df-ibl 21220 . . 3 MblFn
2220, 21elrab2 3218 . 2 MblFn
23 isibl.3 . . . . . . . . . . . 12
2423eleq2d 2521 . . . . . . . . . . 11
2524anbi1d 704 . . . . . . . . . 10
2625ifbid 3911 . . . . . . . . 9
27 isibl.4 . . . . . . . . . . . . 13
2827oveq1d 6207 . . . . . . . . . . . 12
2928fveq2d 5795 . . . . . . . . . . 11
30 isibl.2 . . . . . . . . . . 11
3129, 30eqtr4d 2495 . . . . . . . . . 10
3231ibllem 21360 . . . . . . . . 9
3326, 32eqtrd 2492 . . . . . . . 8
3433mpteq2dv 4479 . . . . . . 7
35 isibl.1 . . . . . . 7
3634, 35eqtr4d 2495 . . . . . 6
3736fveq2d 5795 . . . . 5
3837eleq1d 2520 . . . 4
3938ralbidv 2838 . . 3
4039anbi2d 703 . 2 MblFn MblFn
4122, 40syl5bb 257 1 MblFn
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 184   wa 369   wceq 1370   wcel 1758  wral 2795  csb 3388  cif 3891   class class class wbr 4392   cmpt 4450   cdm 4940  cfv 5518  (class class class)co 6192  cr 9384  cc0 9385  ci 9387   cle 9522   cdiv 10096  c3 10475  cfz 11540  cexp 11968  cre 12690  MblFncmbf 21212  citg2 21214  cibl 21215 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-nul 4521 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2264  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ne 2646  df-ral 2800  df-rex 2801  df-rab 2804  df-v 3072  df-sbc 3287  df-csb 3389  df-dif 3431  df-un 3433  df-in 3435  df-ss 3442  df-nul 3738  df-if 3892  df-sn 3978  df-pr 3980  df-op 3984  df-uni 4192  df-br 4393  df-opab 4451  df-mpt 4452  df-dm 4950  df-iota 5481  df-fv 5526  df-ov 6195  df-ibl 21220 This theorem is referenced by:  isibl2  21362  ibl0  21382
 Copyright terms: Public domain W3C validator