Mathbox for Jeff Madsen < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-pridl Structured version   Unicode version

Definition df-pridl 32145
 Description: Define the class of prime ideals of a ring . A proper ideal of is prime if whenever for ideals and , either or . The more familiar definition using elements rather than ideals is equivalent provided is commutative; see ispridl2 32172 and ispridlc 32204. (Contributed by Jeff Madsen, 10-Jun-2010.)
Assertion
Ref Expression
df-pridl
Distinct variable group:   ,,,,,

Detailed syntax breakdown of Definition df-pridl
StepHypRef Expression
1 cpridl 32142 . 2
2 vr . . 3
3 crngo 26038 . . 3
4 vi . . . . . . 7
54cv 1436 . . . . . 6
62cv 1436 . . . . . . . 8
7 c1st 6742 . . . . . . . 8
86, 7cfv 5537 . . . . . . 7
98crn 4790 . . . . . 6
105, 9wne 2593 . . . . 5
11 vx . . . . . . . . . . . . 13
1211cv 1436 . . . . . . . . . . . 12
13 vy . . . . . . . . . . . . 13
1413cv 1436 . . . . . . . . . . . 12
15 c2nd 6743 . . . . . . . . . . . . 13
166, 15cfv 5537 . . . . . . . . . . . 12
1712, 14, 16co 6242 . . . . . . . . . . 11
1817, 5wcel 1872 . . . . . . . . . 10
19 vb . . . . . . . . . . 11
2019cv 1436 . . . . . . . . . 10
2118, 13, 20wral 2708 . . . . . . . . 9
22 va . . . . . . . . . 10
2322cv 1436 . . . . . . . . 9
2421, 11, 23wral 2708 . . . . . . . 8
2523, 5wss 3372 . . . . . . . . 9
2620, 5wss 3372 . . . . . . . . 9
2725, 26wo 369 . . . . . . . 8
2824, 27wi 4 . . . . . . 7
29 cidl 32141 . . . . . . . 8
306, 29cfv 5537 . . . . . . 7
3128, 19, 30wral 2708 . . . . . 6
3231, 22, 30wral 2708 . . . . 5
3310, 32wa 370 . . . 4
3433, 4, 30crab 2712 . . 3
352, 3, 34cmpt 4418 . 2
361, 35wceq 1437 1
 Colors of variables: wff setvar class This definition is referenced by:  pridlval  32167
 Copyright terms: Public domain W3C validator