Metamath Proof Explorer


Definition df-cndprob

Description: Define the conditional probability. (Contributed by Thierry Arnoux, 14-Sep-2016) (Revised by Thierry Arnoux, 21-Jan-2017)

Ref Expression
Assertion df-cndprob cProb=pProbadomp,bdomppabpb

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccprob classcProb
1 vp setvarp
2 cprb classProb
3 va setvara
4 1 cv setvarp
5 4 cdm classdomp
6 vb setvarb
7 3 cv setvara
8 6 cv setvarb
9 7 8 cin classab
10 9 4 cfv classpab
11 cdiv class÷
12 8 4 cfv classpb
13 10 12 11 co classpabpb
14 3 6 5 5 13 cmpo classadomp,bdomppabpb
15 1 2 14 cmpt classpProbadomp,bdomppabpb
16 0 15 wceq wffcProb=pProbadomp,bdomppabpb