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

Definition df-fae 29064
 Description: Define a builder for an 'almost everywhere' relation between functions, from relations between function values. In this definition, the range of and is enforced in order to ensure the resulting relation is a set. (Contributed by Thierry Arnoux, 22-Oct-2017.)
Assertion
Ref Expression
df-fae ~ a.e. measures a.e.
Distinct variable group:   ,,,,

Detailed syntax breakdown of Definition df-fae
StepHypRef Expression
1 cfae 29057 . 2 ~ a.e.
2 vr . . 3
3 vm . . 3
4 cvv 3081 . . 3
5 cmeas 29013 . . . . 5 measures
65crn 4851 . . . 4 measures
76cuni 4216 . . 3 measures
8 vf . . . . . . . 8
98cv 1436 . . . . . . 7
102cv 1436 . . . . . . . . 9
1110cdm 4850 . . . . . . . 8
123cv 1436 . . . . . . . . . 10
1312cdm 4850 . . . . . . . . 9
1413cuni 4216 . . . . . . . 8
15 cmap 7477 . . . . . . . 8
1611, 14, 15co 6302 . . . . . . 7
179, 16wcel 1868 . . . . . 6
18 vg . . . . . . . 8
1918cv 1436 . . . . . . 7
2019, 16wcel 1868 . . . . . 6
2117, 20wa 370 . . . . 5
22 vx . . . . . . . . . 10
2322cv 1436 . . . . . . . . 9
2423, 9cfv 5598 . . . . . . . 8
2523, 19cfv 5598 . . . . . . . 8
2624, 25, 10wbr 4420 . . . . . . 7
2726, 22, 14crab 2779 . . . . . 6
28 cae 29056 . . . . . 6 a.e.
2927, 12, 28wbr 4420 . . . . 5 a.e.
3021, 29wa 370 . . . 4 a.e.
3130, 8, 18copab 4478 . . 3 a.e.
322, 3, 4, 7, 31cmpt2 6304 . 2 measures a.e.
331, 32wceq 1437 1 ~ a.e. measures a.e.
 Colors of variables: wff setvar class This definition is referenced by:  faeval  29065
 Copyright terms: Public domain W3C validator