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	relopabiv	⊢ Rel a.e.