Theorem probnul

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

	Ref	Expression
Assertion	probnul	$$⊢P\in \mathrm{Prob}\to P\left(\varnothing \right)=0$$

Proof

Step	Hyp	Ref	Expression
1		domprobmeas	$$⊢P\in \mathrm{Prob}\to P\in \mathrm{measures}\left(\mathrm{dom}P\right)$$
2		measvnul	$$⊢P\in \mathrm{measures}\left(\mathrm{dom}P\right)\to P\left(\varnothing \right)=0$$
3	1 2	syl	$$⊢P\in \mathrm{Prob}\to P\left(\varnothing \right)=0$$