Metamath Proof Explorer

Theorem nuleldmp

Description: The empty set is an element of the domain of the probability. (Contributed by Thierry Arnoux, 22-Jan-2017)

		Ref	Expression
	Assertion	nuleldmp	$⊢ P \in Prob \to \emptyset \in dom P$

Step	Hyp	Ref	Expression
1		domprobsiga	$⊢ P \in Prob \to dom P \in ⋃ ran sigAlgebra$
2		0elsiga	$⊢ dom P \in ⋃ ran sigAlgebra \to \emptyset \in dom P$
3	1 2	syl	$⊢ P \in Prob \to \emptyset \in dom P$