Metamath Proof Explorer


Theorem brae

Description: 'almost everywhere' relation for a measure and a measurable set A . (Contributed by Thierry Arnoux, 20-Oct-2017)

Ref Expression
Assertion brae M ran measures A dom M A M-ae. M dom M A = 0

Proof

Step Hyp Ref Expression
1 simpr a = A m = M m = M
2 1 dmeqd a = A m = M dom m = dom M
3 2 unieqd a = A m = M dom m = dom M
4 simpl a = A m = M a = A
5 3 4 difeq12d a = A m = M dom m a = dom M A
6 1 5 fveq12d a = A m = M m dom m a = M dom M A
7 6 eqeq1d a = A m = M m dom m a = 0 M dom M A = 0
8 df-ae ae = a m | m dom m a = 0
9 7 8 brabga A dom M M ran measures A M-ae. M dom M A = 0
10 9 ancoms M ran measures A dom M A M-ae. M dom M A = 0