Metamath Proof Explorer

Theorem probnul

Description: The probability of the empty event set is 0. (Contributed by Thierry Arnoux, 25-Dec-2016)

Ref Expression
Assertion probnul ⊢ P ∈ Prob → P ⁡ ∅ = 0

Proof

Step Hyp Ref Expression
1 domprobmeas ⊢ P ∈ Prob → P ∈ measures ⁡ dom ⁡ P
2 measvnul ⊢ P ∈ measures ⁡ dom ⁡ P → P ⁡ ∅ = 0
3 1 2 syl ⊢ P ∈ Prob → P ⁡ ∅ = 0