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 ( 𝜑𝑃 ∈ Prob )
rrvvf.1 ( 𝜑𝑋 ∈ ( rRndVar ‘ 𝑃 ) )
Assertion rrvdmss ( 𝜑 dom 𝑃 ⊆ dom 𝑋 )

Proof

Step Hyp Ref Expression
1 isrrvv.1 ( 𝜑𝑃 ∈ Prob )
2 rrvvf.1 ( 𝜑𝑋 ∈ ( rRndVar ‘ 𝑃 ) )
3 1 2 rrvdm ( 𝜑 → dom 𝑋 = dom 𝑃 )
4 eqimss2 ( dom 𝑋 = dom 𝑃 dom 𝑃 ⊆ dom 𝑋 )
5 3 4 syl ( 𝜑 dom 𝑃 ⊆ dom 𝑋 )