Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-dvdsr Structured version   Unicode version

Definition df-dvdsr 15746
 Description: Define the (right) divisibility relation in a ring. Access to the left divisibility relation is available through roppr. (Contributed by Mario Carneiro, 1-Dec-2014.)
Assertion
Ref Expression
df-dvdsr r
Distinct variable group:   ,,,

Detailed syntax breakdown of Definition df-dvdsr
StepHypRef Expression
1 cdsr 15743 . 2 r
2 vw . . 3
3 cvv 2956 . . 3
4 vx . . . . . . 7
54cv 1651 . . . . . 6
62cv 1651 . . . . . . 7
7 cbs 13469 . . . . . . 7
86, 7cfv 5454 . . . . . 6
95, 8wcel 1725 . . . . 5
10 vz . . . . . . . . 9
1110cv 1651 . . . . . . . 8
12 cmulr 13530 . . . . . . . . 9
136, 12cfv 5454 . . . . . . . 8
1411, 5, 13co 6081 . . . . . . 7
15 vy . . . . . . . 8
1615cv 1651 . . . . . . 7
1714, 16wceq 1652 . . . . . 6
1817, 10, 8wrex 2706 . . . . 5
199, 18wa 359 . . . 4
2019, 4, 15copab 4265 . . 3
212, 3, 20cmpt 4266 . 2
221, 21wceq 1652 1 r
 Colors of variables: wff set class This definition is referenced by:  reldvdsr  15749  dvdsrval  15750
 Copyright terms: Public domain W3C validator