Definition df-ae 31500

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 31498	. 2 class a.e.
2		vm	. . . . . . . . 9 setvar 𝑚
3	2	cv 1536	. . . . . . . 8 class 𝑚
4	3	cdm 5557	. . . . . . 7 class dom 𝑚
5	4	cuni 4840	. . . . . 6 class ∪ dom 𝑚
6		va	. . . . . . 7 setvar 𝑎
7	6	cv 1536	. . . . . 6 class 𝑎
8	5, 7	cdif 3935	. . . . 5 class (∪ dom 𝑚 ∖ 𝑎)
9	8, 3	cfv 6357	. . . 4 class (𝑚‘(∪ dom 𝑚 ∖ 𝑎))
10		cc0 10539	. . . 4 class 0
11	9, 10	wceq 1537	. . 3 wff (𝑚‘(∪ dom 𝑚 ∖ 𝑎)) = 0
12	11, 6, 2	copab 5130	. 2 class {⟨𝑎, 𝑚⟩ ∣ (𝑚‘(∪ dom 𝑚 ∖ 𝑎)) = 0}
13	1, 12	wceq 1537	1 wff a.e. = {⟨𝑎, 𝑚⟩ ∣ (𝑚‘(∪ dom 𝑚 ∖ 𝑎)) = 0}

This definition is referenced by:  relae  31501  brae  31502  braew  31503