Theorem reldvds

Description: The divides relation is in fact a relation. (Contributed by Steve Rodriguez, 20-Jan-2020)

	Ref	Expression
Assertion	reldvds	$$⊢\mathrm{Rel}\parallel$$

Proof

Step	Hyp	Ref	Expression
1		df-dvds	$$⊢\parallel =\left\{⟨x,y⟩|\left(\left(x\in \mathbb{Z}\wedge y\in \mathbb{Z}\right)\wedge \exists z\in \mathbb{Z}zx=y\right)\right\}$$
2	1	relopabiv	$$⊢\mathrm{Rel}\parallel$$