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

Definition df-domn 17802
 Description: A domain is a nonzero ring in which there are no nontrivial zero divisors. (Contributed by Mario Carneiro, 28-Mar-2015.)
Assertion
Ref Expression
df-domn Domn NzRing
Distinct variable group:   ,,,,

Detailed syntax breakdown of Definition df-domn
StepHypRef Expression
1 cdomn 17798 . 2 Domn
2 vx . . . . . . . . . . 11
32cv 1378 . . . . . . . . . 10
4 vy . . . . . . . . . . 11
54cv 1378 . . . . . . . . . 10
6 vr . . . . . . . . . . . 12
76cv 1378 . . . . . . . . . . 11
8 cmulr 14573 . . . . . . . . . . 11
97, 8cfv 5594 . . . . . . . . . 10
103, 5, 9co 6295 . . . . . . . . 9
11 vz . . . . . . . . . 10
1211cv 1378 . . . . . . . . 9
1310, 12wceq 1379 . . . . . . . 8
142, 11weq 1705 . . . . . . . . 9
154, 11weq 1705 . . . . . . . . 9
1614, 15wo 368 . . . . . . . 8
1713, 16wi 4 . . . . . . 7
18 vb . . . . . . . 8
1918cv 1378 . . . . . . 7
2017, 4, 19wral 2817 . . . . . 6
2120, 2, 19wral 2817 . . . . 5
22 c0g 14712 . . . . . 6
237, 22cfv 5594 . . . . 5
2421, 11, 23wsbc 3336 . . . 4
25 cbs 14507 . . . . 5
267, 25cfv 5594 . . . 4
2724, 18, 26wsbc 3336 . . 3
28 cnzr 17775 . . 3 NzRing
2927, 6, 28crab 2821 . 2 NzRing
301, 29wceq 1379 1 Domn NzRing
 Colors of variables: wff setvar class This definition is referenced by:  isdomn  17813
 Copyright terms: Public domain W3C validator