Definition df-cndprob 30494

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 = ( p e. Prob |-> ( a e. dom p , b e. dom p |-> ( ( p ` ( a i^i b ) ) / ( p ` b ) ) ) )

Distinct variable group:   a, b, p

Detailed syntax breakdown of Definition df-cndprob

Step	Hyp	Ref	Expression
1		ccprob 30493	. 2 class cprob
2		vp	. . 3 setvar p
3		cprb 30469	. . 3 class Prob
4		va	. . . 4 setvar a
5		vb	. . . 4 setvar b
6	2	cv 1482	. . . . 5 class p
7	6	cdm 5114	. . . 4 class dom p
8	4	cv 1482	. . . . . . 7 class a
9	5	cv 1482	. . . . . . 7 class b
10	8, 9	cin 3573	. . . . . 6 class ( a i^i b )
11	10, 6	cfv 5888	. . . . 5 class ( p ` ( a i^i b ) )
12	9, 6	cfv 5888	. . . . 5 class ( p ` b )
13		cdiv 10684	. . . . 5 class /
14	11, 12, 13	co 6650	. . . 4 class ( ( p ` ( a i^i b ) ) / ( p ` b ) )
15	4, 5, 7, 7, 14	cmpt2 6652	. . 3 class ( a e. dom p , b e. dom p |-> ( ( p ` ( a i^i b ) ) / ( p ` b ) ) )
16	2, 3, 15	cmpt 4729	. 2 class ( p e. Prob |-> ( a e. dom p , b e. dom p |-> ( ( p ` ( a i^i b ) ) / ( p ` b ) ) ) )
17	1, 16	wceq 1483	1 wff cprob = ( p e. Prob |-> ( a e. dom p , b e. dom p |-> ( ( p ` ( a i^i b ) ) / ( p ` b ) ) ) )

This definition is referenced by:  cndprobval  30495