Mathbox for Thierry Arnoux < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  measvnul Structured version   Unicode version

Theorem measvnul 28047
 Description: The measure of the empty set is always zero. (Contributed by Thierry Arnoux, 26-Dec-2016.)
Assertion
Ref Expression
measvnul measures

Proof of Theorem measvnul
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 measbase 28038 . . . 4 measures sigAlgebra
2 ismeas 28040 . . . 4 sigAlgebra measures Disj Σ*
31, 2syl 16 . . 3 measures measures Disj Σ*
43ibi 241 . 2 measures Disj Σ*
54simp2d 1008 1 measures
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 184   wa 369   w3a 972   wceq 1381   wcel 1802  wral 2791  c0 3768  cpw 3994  cuni 4231  Disj wdisj 4404   class class class wbr 4434   crn 4987  wf 5571  cfv 5575  (class class class)co 6278  com 6682   cdom 7513  cc0 9492   cpnf 9625  cicc 11538  Σ*cesum 27910  sigAlgebracsiga 27977  measurescmeas 28036 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-8 1804  ax-9 1806  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419  ax-sep 4555  ax-nul 4563  ax-pow 4612  ax-pr 4673  ax-un 6574 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 974  df-tru 1384  df-fal 1387  df-ex 1598  df-nf 1602  df-sb 1725  df-eu 2270  df-mo 2271  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ne 2638  df-ral 2796  df-rex 2797  df-rab 2800  df-v 3095  df-sbc 3312  df-csb 3419  df-dif 3462  df-un 3464  df-in 3466  df-ss 3473  df-nul 3769  df-if 3924  df-pw 3996  df-sn 4012  df-pr 4014  df-op 4018  df-uni 4232  df-br 4435  df-opab 4493  df-mpt 4494  df-id 4782  df-xp 4992  df-rel 4993  df-cnv 4994  df-co 4995  df-dm 4996  df-rn 4997  df-iota 5538  df-fun 5577  df-fn 5578  df-f 5579  df-fv 5583  df-ov 6281  df-esum 27911  df-meas 28037 This theorem is referenced by:  measxun2  28051  measvunilem0  28054  measssd  28056  measinb  28062  measres  28063  measdivcstOLD  28065  measdivcst  28066  truae  28085  probnul  28223
 Copyright terms: Public domain W3C validator