Theorem relae

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

	Ref	Expression
Assertion	relae	$$⊢\mathrm{Rel}\mathrm{ae}$$

Proof

Step	Hyp	Ref	Expression
1		df-ae	$$⊢\mathrm{ae}=\left\{⟨a,m⟩|m\left(\bigcup \mathrm{dom}m\setminus a\right)=0\right\}$$
2	1	relopabiv	$$⊢\mathrm{Rel}\mathrm{ae}$$