Description: Define the conditional probability. (Contributed by Thierry Arnoux, 14-Sep-2016) (Revised by Thierry Arnoux, 21-Jan-2017)
Ref | Expression | ||
---|---|---|---|
Assertion | df-cndprob | |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | ccprob | |
|
1 | vp | |
|
2 | cprb | |
|
3 | va | |
|
4 | 1 | cv | |
5 | 4 | cdm | |
6 | vb | |
|
7 | 3 | cv | |
8 | 6 | cv | |
9 | 7 8 | cin | |
10 | 9 4 | cfv | |
11 | cdiv | |
|
12 | 8 4 | cfv | |
13 | 10 12 11 | co | |
14 | 3 6 5 5 13 | cmpo | |
15 | 1 2 14 | cmpt | |
16 | 0 15 | wceq | |