Definition df-prmring

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) (Revised by AV, 18-Jun-2026)

	Ref	Expression
Assertion	df-prmring	|- PrmRing = { r e. Ring | { ( 0g ` r ) } e. ( PrmIdeal ` r ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cprmrng	|- PrmRing
1		vr	|- r
2		crg	|- Ring
3		c0g	|- 0g
4	1	cv	|- r
5	4 3	cfv	|- ( 0g ` r )
6	5	csn	|- { ( 0g ` r ) }
7		cprmidl	|- PrmIdeal
8	4 7	cfv	|- ( PrmIdeal ` r )
9	6 8	wcel	|- { ( 0g ` r ) } e. ( PrmIdeal ` r )
10	9 1 2	crab	|- { r e. Ring | { ( 0g ` r ) } e. ( PrmIdeal ` r ) }
11	0 10	wceq	|- PrmRing = { r e. Ring | { ( 0g ` r ) } e. ( PrmIdeal ` r ) }