Description: The divides relation is in fact a relation. (Contributed by Steve Rodriguez, 20-Jan-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | reldvds | ⊢ Rel ∥ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-dvds | ⊢ ∥ = { 〈 𝑥 , 𝑦 〉 ∣ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ ∃ 𝑧 ∈ ℤ ( 𝑧 · 𝑥 ) = 𝑦 ) } | |
2 | 1 | relopabiv | ⊢ Rel ∥ |