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 dom m a = 0
2 1 relopabiv Rel ae