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 | |- || = { <. x , y >. | ( ( x e. ZZ /\ y e. ZZ ) /\ E. z e. ZZ ( z x. x ) = y ) } |
|
2 | 1 | relopabiv | |- Rel || |