Metamath Proof Explorer


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 φ P Prob
rrvvf.1 φ X RndVar P
Assertion rrvdmss φ dom P dom X

Proof

Step Hyp Ref Expression
1 isrrvv.1 φ P Prob
2 rrvvf.1 φ X RndVar P
3 1 2 rrvdm φ dom X = dom P
4 eqimss2 dom X = dom P dom P dom X
5 3 4 syl φ dom P dom X