# Metamath Proof Explorer

## Definition df-prob

Description: Define the class of probability measures as the set of measures with total measure 1. (Contributed by Thierry Arnoux, 14-Sep-2016)

Ref Expression
Assertion df-prob ${⊢}\mathrm{Prob}=\left\{{p}\in \bigcup \mathrm{ran}\mathrm{measures}|{p}\left(\bigcup \mathrm{dom}{p}\right)=1\right\}$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 cprb ${class}\mathrm{Prob}$
1 vp ${setvar}{p}$
2 cmeas ${class}\mathrm{measures}$
3 2 crn ${class}\mathrm{ran}\mathrm{measures}$
4 3 cuni ${class}\bigcup \mathrm{ran}\mathrm{measures}$
5 1 cv ${setvar}{p}$
6 5 cdm ${class}\mathrm{dom}{p}$
7 6 cuni ${class}\bigcup \mathrm{dom}{p}$
8 7 5 cfv ${class}{p}\left(\bigcup \mathrm{dom}{p}\right)$
9 c1 ${class}1$
10 8 9 wceq ${wff}{p}\left(\bigcup \mathrm{dom}{p}\right)=1$
11 10 1 4 crab ${class}\left\{{p}\in \bigcup \mathrm{ran}\mathrm{measures}|{p}\left(\bigcup \mathrm{dom}{p}\right)=1\right\}$
12 0 11 wceq ${wff}\mathrm{Prob}=\left\{{p}\in \bigcup \mathrm{ran}\mathrm{measures}|{p}\left(\bigcup \mathrm{dom}{p}\right)=1\right\}$