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	$$⊢\mathrm{cProb}=\left(p\in \mathrm{Prob}⟼\left(a\in \mathrm{dom}p,b\in \mathrm{dom}p⟼\frac{p\left(a\cap b\right)}{p\left(b\right)}\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccprob	$$class\mathrm{cProb}$$
1		vp	$$setvarp$$
2		cprb	$$class\mathrm{Prob}$$
3		va	$$setvara$$
4	1	cv	$$setvarp$$
5	4	cdm	$$class\mathrm{dom}p$$
6		vb	$$setvarb$$
7	3	cv	$$setvara$$
8	6	cv	$$setvarb$$
9	7 8	cin	$$class\left(a\cap b\right)$$
10	9 4	cfv	$$classp\left(a\cap b\right)$$
11		cdiv	$$class÷$$
12	8 4	cfv	$$classp\left(b\right)$$
13	10 12 11	co	$$class\left(\frac{p\left(a\cap b\right)}{p\left(b\right)}\right)$$
14	3 6 5 5 13	cmpo	$$class\left(a\in \mathrm{dom}p,b\in \mathrm{dom}p⟼\frac{p\left(a\cap b\right)}{p\left(b\right)}\right)$$
15	1 2 14	cmpt	$$class\left(p\in \mathrm{Prob}⟼\left(a\in \mathrm{dom}p,b\in \mathrm{dom}p⟼\frac{p\left(a\cap b\right)}{p\left(b\right)}\right)\right)$$
16	0 15	wceq	$$wff\mathrm{cProb}=\left(p\in \mathrm{Prob}⟼\left(a\in \mathrm{dom}p,b\in \mathrm{dom}p⟼\frac{p\left(a\cap b\right)}{p\left(b\right)}\right)\right)$$