Metamath Proof Explorer


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 ∥