Metamath Proof Explorer


Theorem ddeval0

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

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

Proof

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