Metamath Proof Explorer

Theorem relae

Description: 'almost everywhere' is a relation. (Contributed by Thierry Arnoux, 20-Oct-2017)

Ref Expression
Assertion relae 
|- Rel ae

Proof

Step Hyp Ref Expression
1 df-ae 
 |-  ae = { <. a , m >. | ( m ` ( U. dom m \ a ) ) = 0 }
2 1 relopabiv 
 |-  Rel ae