# Metamath Proof Explorer

## Theorem ddeval1

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

Ref Expression
Assertion ddeval1 ${⊢}\left({A}\subseteq ℝ\wedge 0\in {A}\right)\to \delta \left({A}\right)=1$

### Proof

Step Hyp Ref Expression
1 reex ${⊢}ℝ\in \mathrm{V}$
2 1 ssex ${⊢}{A}\subseteq ℝ\to {A}\in \mathrm{V}$
3 elpwg ${⊢}{A}\in \mathrm{V}\to \left({A}\in 𝒫ℝ↔{A}\subseteq ℝ\right)$
4 3 biimpar ${⊢}\left({A}\in \mathrm{V}\wedge {A}\subseteq ℝ\right)\to {A}\in 𝒫ℝ$
5 2 4 mpancom ${⊢}{A}\subseteq ℝ\to {A}\in 𝒫ℝ$
6 eleq2 ${⊢}{a}={A}\to \left(0\in {a}↔0\in {A}\right)$
7 6 ifbid ${⊢}{a}={A}\to if\left(0\in {a},1,0\right)=if\left(0\in {A},1,0\right)$
8 df-dde ${⊢}\delta =\left({a}\in 𝒫ℝ⟼if\left(0\in {a},1,0\right)\right)$
9 1ex ${⊢}1\in \mathrm{V}$
10 c0ex ${⊢}0\in \mathrm{V}$
11 9 10 ifex ${⊢}if\left(0\in {A},1,0\right)\in \mathrm{V}$
12 7 8 11 fvmpt ${⊢}{A}\in 𝒫ℝ\to \delta \left({A}\right)=if\left(0\in {A},1,0\right)$
13 5 12 syl ${⊢}{A}\subseteq ℝ\to \delta \left({A}\right)=if\left(0\in {A},1,0\right)$
14 iftrue ${⊢}0\in {A}\to if\left(0\in {A},1,0\right)=1$
15 13 14 sylan9eq ${⊢}\left({A}\subseteq ℝ\wedge 0\in {A}\right)\to \delta \left({A}\right)=1$