Description: The value of the distribution of a random variable. (Contributed by Thierry Arnoux, 9-Feb-2017)
Ref | Expression | ||
---|---|---|---|
Hypotheses | dstrvprob.1 | |
|
dstrvprob.2 | |
||
dstrvprob.3 | |
||
dstrvval.1 | |
||
Assertion | dstrvval | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dstrvprob.1 | |
|
2 | dstrvprob.2 | |
|
3 | dstrvprob.3 | |
|
4 | dstrvval.1 | |
|
5 | 3 | fveq1d | |
6 | oveq2 | |
|
7 | 6 | fveq2d | |
8 | eqid | |
|
9 | fvex | |
|
10 | 7 8 9 | fvmpt | |
11 | 4 10 | syl | |
12 | 1 2 4 | orvcelval | |
13 | 12 | fveq2d | |
14 | 5 11 13 | 3eqtrd | |