Theorem elprob

Description: The property of being a probability measure. (Contributed by Thierry Arnoux, 8-Dec-2016)

	Ref	Expression
Assertion	elprob	|- ( P e. Prob <-> ( P e. U. ran measures /\ ( P ` U. dom P ) = 1 ) )

Proof

Step	Hyp	Ref	Expression
1		id	|- ( p = P -> p = P )
2		dmeq	|- ( p = P -> dom p = dom P )
3	2	unieqd	|- ( p = P -> U. dom p = U. dom P )
4	1 3	fveq12d	|- ( p = P -> ( p ` U. dom p ) = ( P ` U. dom P ) )
5	4	eqeq1d	|- ( p = P -> ( ( p ` U. dom p ) = 1 <-> ( P ` U. dom P ) = 1 ) )
6		df-prob	|- Prob = { p e. U. ran measures | ( p ` U. dom p ) = 1 }
7	5 6	elrab2	|- ( P e. Prob <-> ( P e. U. ran measures /\ ( P ` U. dom P ) = 1 ) )