Metamath Proof Explorer


Theorem relae

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

Ref Expression
Assertion relae Rel a.e.

Proof

Step Hyp Ref Expression
1 df-ae a.e. = { ⟨ 𝑎 , 𝑚 ⟩ ∣ ( 𝑚 ‘ ( dom 𝑚𝑎 ) ) = 0 }
2 1 relopabi Rel a.e.