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	⊢ ∥ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ ∃ 𝑧 ∈ ℤ ( 𝑧 · 𝑥 ) = 𝑦 ) }
2	1	relopabiv	⊢ Rel ∥