Definition df-cndprob 32111

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 32110	. 2 class cprob
2		vp	. . 3 setvar 𝑝
3		cprb 32086	. . 3 class Prob
4		va	. . . 4 setvar 𝑎
5		vb	. . . 4 setvar 𝑏
6	2	cv 1542	. . . . 5 class 𝑝
7	6	cdm 5551	. . . 4 class dom 𝑝
8	4	cv 1542	. . . . . . 7 class 𝑎
9	5	cv 1542	. . . . . . 7 class 𝑏
10	8, 9	cin 3865	. . . . . 6 class (𝑎 ∩ 𝑏)
11	10, 6	cfv 6380	. . . . 5 class (𝑝‘(𝑎 ∩ 𝑏))
12	9, 6	cfv 6380	. . . . 5 class (𝑝‘𝑏)
13		cdiv 11489	. . . . 5 class /
14	11, 12, 13	co 7213	. . . 4 class ((𝑝‘(𝑎 ∩ 𝑏)) / (𝑝‘𝑏))
15	4, 5, 7, 7, 14	cmpo 7215	. . 3 class (𝑎 ∈ dom 𝑝, 𝑏 ∈ dom 𝑝 ↦ ((𝑝‘(𝑎 ∩ 𝑏)) / (𝑝‘𝑏)))
16	2, 3, 15	cmpt 5135	. 2 class (𝑝 ∈ Prob ↦ (𝑎 ∈ dom 𝑝, 𝑏 ∈ dom 𝑝 ↦ ((𝑝‘(𝑎 ∩ 𝑏)) / (𝑝‘𝑏))))
17	1, 16	wceq 1543	1 wff cprob = (𝑝 ∈ Prob ↦ (𝑎 ∈ dom 𝑝, 𝑏 ∈ dom 𝑝 ↦ ((𝑝‘(𝑎 ∩ 𝑏)) / (𝑝‘𝑏))))

This definition is referenced by:  cndprobval  32112