Definition df-prrngo

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)

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cprrng	|- PrRing
1		vr	|- r
2		crngo	|- RingOps
3		cgi	|- GId
4		c1st	|- 1st
5	1	cv	|- r
6	5 4	cfv	|- ( 1st ` r )
7	6 3	cfv	|- ( GId ` ( 1st ` r ) )
8	7	csn	|- { ( GId ` ( 1st ` r ) ) }
9		cpridl	|- PrIdl
10	5 9	cfv	|- ( PrIdl ` r )
11	8 10	wcel	|- { ( GId ` ( 1st ` r ) ) } e. ( PrIdl ` r )
12	11 1 2	crab	|- { r e. RingOps | { ( GId ` ( 1st ` r ) ) } e. ( PrIdl ` r ) }
13	0 12	wceq	|- PrRing = { r e. RingOps | { ( GId ` ( 1st ` r ) ) } e. ( PrIdl ` r ) }