Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-cndprob Structured version   Visualization version   GIF version

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
StepHypRef 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 𝑏
62cv 1542 . . . . 5 class 𝑝
76cdm 5551 . . . 4 class dom 𝑝
84cv 1542 . . . . . . 7 class 𝑎
95cv 1542 . . . . . . 7 class 𝑏
108, 9cin 3865 . . . . . 6 class (𝑎𝑏)
1110, 6cfv 6380 . . . . 5 class (𝑝‘(𝑎𝑏))
129, 6cfv 6380 . . . . 5 class (𝑝𝑏)
13 cdiv 11489 . . . . 5 class /
1411, 12, 13co 7213 . . . 4 class ((𝑝‘(𝑎𝑏)) / (𝑝𝑏))
154, 5, 7, 7, 14cmpo 7215 . . 3 class (𝑎 ∈ dom 𝑝, 𝑏 ∈ dom 𝑝 ↦ ((𝑝‘(𝑎𝑏)) / (𝑝𝑏)))
162, 3, 15cmpt 5135 . 2 class (𝑝 ∈ Prob ↦ (𝑎 ∈ dom 𝑝, 𝑏 ∈ dom 𝑝 ↦ ((𝑝‘(𝑎𝑏)) / (𝑝𝑏))))
171, 16wceq 1543 1 wff cprob = (𝑝 ∈ Prob ↦ (𝑎 ∈ dom 𝑝, 𝑏 ∈ dom 𝑝 ↦ ((𝑝‘(𝑎𝑏)) / (𝑝𝑏))))
Colors of variables: wff setvar class
This definition is referenced by:  cndprobval  32112
  Copyright terms: Public domain W3C validator