Theorem reldvds

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

	Ref	Expression
Assertion	reldvds	|- Rel ||

Proof

Step	Hyp	Ref	Expression
1		df-dvds	|- || = { <. x , y >. | ( ( x e. ZZ /\ y e. ZZ ) /\ E. z e. ZZ ( z x. x ) = y ) }
2	1	relopabiv	|- Rel ||