Definition df-ae 31491

Description: Define 'almost everywhere' with regard to a measure 𝑀. A property holds almost everywhere if the measure of the set where it does not hold has measure zero. (Contributed by Thierry Arnoux, 20-Oct-2017.)

Assertion

Ref	Expression
df-ae	⊢ a.e. = {⟨𝑎, 𝑚⟩ ∣ (𝑚‘(∪ dom 𝑚 ∖ 𝑎)) = 0}

Distinct variable group:   𝑚,𝑎

Detailed syntax breakdown of Definition df-ae

Step	Hyp	Ref	Expression
1		cae 31489	. 2 class a.e.
2		vm	. . . . . . . . 9 setvar 𝑚
3	2	cv 1529	. . . . . . . 8 class 𝑚
4	3	cdm 5548	. . . . . . 7 class dom 𝑚
5	4	cuni 4830	. . . . . 6 class ∪ dom 𝑚
6		va	. . . . . . 7 setvar 𝑎
7	6	cv 1529	. . . . . 6 class 𝑎
8	5, 7	cdif 3931	. . . . 5 class (∪ dom 𝑚 ∖ 𝑎)
9	8, 3	cfv 6348	. . . 4 class (𝑚‘(∪ dom 𝑚 ∖ 𝑎))
10		cc0 10529	. . . 4 class 0
11	9, 10	wceq 1530	. . 3 wff (𝑚‘(∪ dom 𝑚 ∖ 𝑎)) = 0
12	11, 6, 2	copab 5119	. 2 class {⟨𝑎, 𝑚⟩ ∣ (𝑚‘(∪ dom 𝑚 ∖ 𝑎)) = 0}
13	1, 12	wceq 1530	1 wff a.e. = {⟨𝑎, 𝑚⟩ ∣ (𝑚‘(∪ dom 𝑚 ∖ 𝑎)) = 0}

This definition is referenced by:  relae  31492  brae  31493  braew  31494