Definition df-prmring 48955

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

Assertion

Ref	Expression
df-prmring	⊢ PrmRing = {𝑟 ∈ Ring ∣ {(0g‘𝑟)} ∈ (PrmIdeal‘𝑟)}

Detailed syntax breakdown of Definition df-prmring

Step	Hyp	Ref	Expression
1		cprmrng 48954	. 2 class PrmRing
2		vr	. . . . . . 7 setvar 𝑟
3	2	cv 1562	. . . . . 6 class 𝑟
4		c0g 17482	. . . . . 6 class 0g
5	3, 4	cfv 6525	. . . . 5 class (0g‘𝑟)
6	5	csn 4585	. . . 4 class {(0g‘𝑟)}
7		cprmidl 21422	. . . . 5 class PrmIdeal
8	3, 7	cfv 6525	. . . 4 class (PrmIdeal‘𝑟)
9	6, 8	wcel 2145	. . 3 wff {(0g‘𝑟)} ∈ (PrmIdeal‘𝑟)
10		crg 20306	. . 3 class Ring
11	9, 2, 10	crab 3417	. 2 class {𝑟 ∈ Ring ∣ {(0g‘𝑟)} ∈ (PrmIdeal‘𝑟)}
12	1, 11	wceq 1563	1 wff PrmRing = {𝑟 ∈ Ring ∣ {(0g‘𝑟)} ∈ (PrmIdeal‘𝑟)}

This definition is referenced by:  isprmrng  48956