Theorem rrvdmss

Description: The domain of a random variable. This is useful to shorten proofs. (Contributed by Thierry Arnoux, 25-Jan-2017)

	Ref	Expression
Hypotheses	isrrvv.1	|- ( ph -> P e. Prob )
	rrvvf.1	|- ( ph -> X e. ( rRndVar ` P ) )
Assertion	rrvdmss	|- ( ph -> U. dom P C_ dom X )

Proof

Step	Hyp	Ref	Expression
1		isrrvv.1	|- ( ph -> P e. Prob )
2		rrvvf.1	|- ( ph -> X e. ( rRndVar ` P ) )
3	1 2	rrvdm	|- ( ph -> dom X = U. dom P )
4		eqimss2	|- ( dom X = U. dom P -> U. dom P C_ dom X )
5	3 4	syl	|- ( ph -> U. dom P C_ dom X )