Definition df-prrngo 33847

Description: 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.)

Assertion

Ref	Expression
df-prrngo	|- PrRing = { r e. RingOps | { (GId ` ( 1st ` r ) ) } e. ( PrIdl ` r ) }

Detailed syntax breakdown of Definition df-prrngo

Step	Hyp	Ref	Expression
1		cprrng 33845	. 2 class PrRing
2		vr	. . . . . . . 8 setvar r
3	2	cv 1482	. . . . . . 7 class r
4		c1st 7166	. . . . . . 7 class 1st
5	3, 4	cfv 5888	. . . . . 6 class ( 1st ` r )
6		cgi 27344	. . . . . 6 class GId
7	5, 6	cfv 5888	. . . . 5 class (GId ` ( 1st ` r ) )
8	7	csn 4177	. . . 4 class { (GId ` ( 1st ` r ) ) }
9		cpridl 33807	. . . . 5 class PrIdl
10	3, 9	cfv 5888	. . . 4 class ( PrIdl ` r )
11	8, 10	wcel 1990	. . 3 wff { (GId ` ( 1st ` r ) ) } e. ( PrIdl ` r )
12		crngo 33693	. . 3 class RingOps
13	11, 2, 12	crab 2916	. 2 class { r e. RingOps | { (GId ` ( 1st ` r ) ) } e. ( PrIdl ` r ) }
14	1, 13	wceq 1483	1 wff PrRing = { r e. RingOps | { (GId ` ( 1st ` r ) ) } e. ( PrIdl ` r ) }

This definition is referenced by:  isprrngo  33849