Theorem probnul

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

	Ref	Expression
Assertion	probnul	⊢ ( 𝑃 ∈ Prob → ( 𝑃 ‘ ∅ ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		domprobmeas	⊢ ( 𝑃 ∈ Prob → 𝑃 ∈ ( measures ‘ dom 𝑃 ) )
2		measvnul	⊢ ( 𝑃 ∈ ( measures ‘ dom 𝑃 ) → ( 𝑃 ‘ ∅ ) = 0 )
3	1 2	syl	⊢ ( 𝑃 ∈ Prob → ( 𝑃 ‘ ∅ ) = 0 )