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 e. Prob -> ( P ` (/) ) = 0 )

Proof

Step Hyp Ref Expression
1 domprobmeas 
 |-  ( P e. Prob -> P e. ( measures ` dom P ) )
2 measvnul 
 |-  ( P e. ( measures ` dom P ) -> ( P ` (/) ) = 0 )
3 1 2 syl 
 |-  ( P e. Prob -> ( P ` (/) ) = 0 )