Definition df-cndprob 31692

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

Assertion

Ref	Expression
df-cndprob	⊢ cprob = (𝑝 ∈ Prob ↦ (𝑎 ∈ dom 𝑝, 𝑏 ∈ dom 𝑝 ↦ ((𝑝‘(𝑎 ∩ 𝑏)) / (𝑝‘𝑏))))

Distinct variable group:   𝑎,𝑏,𝑝

Detailed syntax breakdown of Definition df-cndprob

Step	Hyp	Ref	Expression
1		ccprob 31691	. 2 class cprob
2		vp	. . 3 setvar 𝑝
3		cprb 31667	. . 3 class Prob
4		va	. . . 4 setvar 𝑎
5		vb	. . . 4 setvar 𝑏
6	2	cv 1536	. . . . 5 class 𝑝
7	6	cdm 5557	. . . 4 class dom 𝑝
8	4	cv 1536	. . . . . . 7 class 𝑎
9	5	cv 1536	. . . . . . 7 class 𝑏
10	8, 9	cin 3937	. . . . . 6 class (𝑎 ∩ 𝑏)
11	10, 6	cfv 6357	. . . . 5 class (𝑝‘(𝑎 ∩ 𝑏))
12	9, 6	cfv 6357	. . . . 5 class (𝑝‘𝑏)
13		cdiv 11299	. . . . 5 class /
14	11, 12, 13	co 7158	. . . 4 class ((𝑝‘(𝑎 ∩ 𝑏)) / (𝑝‘𝑏))
15	4, 5, 7, 7, 14	cmpo 7160	. . 3 class (𝑎 ∈ dom 𝑝, 𝑏 ∈ dom 𝑝 ↦ ((𝑝‘(𝑎 ∩ 𝑏)) / (𝑝‘𝑏)))
16	2, 3, 15	cmpt 5148	. 2 class (𝑝 ∈ Prob ↦ (𝑎 ∈ dom 𝑝, 𝑏 ∈ dom 𝑝 ↦ ((𝑝‘(𝑎 ∩ 𝑏)) / (𝑝‘𝑏))))
17	1, 16	wceq 1537	1 wff cprob = (𝑝 ∈ Prob ↦ (𝑎 ∈ dom 𝑝, 𝑏 ∈ dom 𝑝 ↦ ((𝑝‘(𝑎 ∩ 𝑏)) / (𝑝‘𝑏))))

This definition is referenced by:  cndprobval  31693