Definition df-prrngo 38740

Description: Obsolete definition, use df-prmring 49141 instead. Define the class of prime rings. A ring is prime if the zero ideal is a prime ideal. (Contributed by Jeff Madsen, 10-Jun-2010.) (New usage is discouraged.)

Assertion

Ref	Expression
df-prrngo	⊢ PrRing = {𝑟 ∈ RingOps ∣ {(GId‘(1st ‘𝑟))} ∈ (PrIdl‘𝑟)}

Detailed syntax breakdown of Definition df-prrngo

Step	Hyp	Ref	Expression
1		cprrng 38738	. 2 class PrRing
2		vr	. . . . . . . 8 setvar 𝑟
3	2	cv 1569	. . . . . . 7 class 𝑟
4		c1st 7993	. . . . . . 7 class 1st
5	3, 4	cfv 6543	. . . . . 6 class (1st ‘𝑟)
6		cgi 30879	. . . . . 6 class GId
7	5, 6	cfv 6543	. . . . 5 class (GId‘(1st ‘𝑟))
8	7	csn 4594	. . . 4 class {(GId‘(1st ‘𝑟))}
9		cpridl 38700	. . . . 5 class PrIdl
10	3, 9	cfv 6543	. . . 4 class (PrIdl‘𝑟)
11	8, 10	wcel 2146	. . 3 wff {(GId‘(1st ‘𝑟))} ∈ (PrIdl‘𝑟)
12		crngo 38586	. . 3 class RingOps
13	11, 2, 12	crab 3419	. 2 class {𝑟 ∈ RingOps ∣ {(GId‘(1st ‘𝑟))} ∈ (PrIdl‘𝑟)}
14	1, 13	wceq 1570	1 wff PrRing = {𝑟 ∈ RingOps ∣ {(GId‘(1st ‘𝑟))} ∈ (PrIdl‘𝑟)}

This definition is used by:  isprrngo  38742