Metamath Proof Explorer


Theorem ddeval0

Description: Value of the delta measure. (Contributed by Thierry Arnoux, 14-Sep-2018)

Ref Expression
Assertion ddeval0 A¬0AδA=0

Proof

Step Hyp Ref Expression
1 reex V
2 1 ssex AAV
3 elpwg AVA𝒫A
4 3 biimpar AVAA𝒫
5 2 4 mpancom AA𝒫
6 eleq2 a=A0a0A
7 6 ifbid a=Aif0a10=if0A10
8 df-dde δ=a𝒫if0a10
9 1ex 1V
10 c0ex 0V
11 9 10 ifex if0A10V
12 7 8 11 fvmpt A𝒫δA=if0A10
13 5 12 syl AδA=if0A10
14 iffalse ¬0Aif0A10=0
15 13 14 sylan9eq A¬0AδA=0