Mathbox for Thierry Arnoux < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  cndprobval Structured version   Unicode version

Theorem cndprobval 26955
 Description: The value of the conditional probability , i.e. the probability for the event , given , under the probability law . (Contributed by Thierry Arnoux, 21-Jan-2017.)
Assertion
Ref Expression
cndprobval Prob cprob

Proof of Theorem cndprobval
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-ov 6198 . 2 cprob cprob
2 df-cndprob 26954 . . . . . 6 cprob Prob
32a1i 11 . . . . 5 Prob cprob Prob
4 dmeq 5143 . . . . . . 7
5 fveq1 5793 . . . . . . . 8
6 fveq1 5793 . . . . . . . 8
75, 6oveq12d 6213 . . . . . . 7
84, 4, 7mpt2eq123dv 6252 . . . . . 6
98adantl 466 . . . . 5 Prob
10 id 22 . . . . 5 Prob Prob
11 dmexg 6614 . . . . . 6 Prob
12 mpt2exga 6754 . . . . . 6
1311, 11, 12syl2anc 661 . . . . 5 Prob
143, 9, 10, 13fvmptd 5883 . . . 4 Prob cprob
15143ad2ant1 1009 . . 3 Prob cprob
16 simprl 755 . . . . . 6 Prob
17 simprr 756 . . . . . 6 Prob
1816, 17ineq12d 3656 . . . . 5 Prob
1918fveq2d 5798 . . . 4 Prob
2017fveq2d 5798 . . . 4 Prob
2119, 20oveq12d 6213 . . 3 Prob
22 simp2 989 . . 3 Prob
23 simp3 990 . . 3 Prob
24 ovex 6220 . . . 4
2524a1i 11 . . 3 Prob
2615, 21, 22, 23, 25ovmpt2d 6323 . 2 Prob cprob
271, 26syl5eqr 2507 1 Prob cprob
 Colors of variables: wff setvar class Syntax hints:   wi 4   wa 369   w3a 965   wceq 1370   wcel 1758  cvv 3072   cin 3430  cop 3986   cmpt 4453   cdm 4943  cfv 5521  (class class class)co 6195   cmpt2 6197   cdiv 10099  Probcprb 26929  cprobccprob 26953 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1954  ax-ext 2431  ax-rep 4506  ax-sep 4516  ax-nul 4524  ax-pow 4573  ax-pr 4634  ax-un 6477 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2265  df-mo 2266  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2602  df-ne 2647  df-ral 2801  df-rex 2802  df-reu 2803  df-rab 2805  df-v 3074  df-sbc 3289  df-csb 3391  df-dif 3434  df-un 3436  df-in 3438  df-ss 3445  df-nul 3741  df-if 3895  df-pw 3965  df-sn 3981  df-pr 3983  df-op 3987  df-uni 4195  df-iun 4276  df-br 4396  df-opab 4454  df-mpt 4455  df-id 4739  df-xp 4949  df-rel 4950  df-cnv 4951  df-co 4952  df-dm 4953  df-rn 4954  df-res 4955  df-ima 4956  df-iota 5484  df-fun 5523  df-fn 5524  df-f 5525  df-f1 5526  df-fo 5527  df-f1o 5528  df-fv 5529  df-ov 6198  df-oprab 6199  df-mpt2 6200  df-1st 6682  df-2nd 6683  df-cndprob 26954 This theorem is referenced by:  cndprobin  26956  cndprob01  26957  cndprobtot  26958  cndprobnul  26959  cndprobprob  26960
 Copyright terms: Public domain W3C validator