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 = { 𝑟 ∈ Ring ∣ { ( 0g ‘ 𝑟 ) } ∈ ( PrmIdeal ‘ 𝑟 ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cprmrng	⊢ PrmRing
1		vr	⊢ 𝑟
2		crg	⊢ Ring
3		c0g	⊢ 0g
4	1	cv	⊢ 𝑟
5	4 3	cfv	⊢ ( 0g ‘ 𝑟 )
6	5	csn	⊢ { ( 0g ‘ 𝑟 ) }
7		cprmidl	⊢ PrmIdeal
8	4 7	cfv	⊢ ( PrmIdeal ‘ 𝑟 )
9	6 8	wcel	⊢ { ( 0g ‘ 𝑟 ) } ∈ ( PrmIdeal ‘ 𝑟 )
10	9 1 2	crab	⊢ { 𝑟 ∈ Ring ∣ { ( 0g ‘ 𝑟 ) } ∈ ( PrmIdeal ‘ 𝑟 ) }
11	0 10	wceq	⊢ PrmRing = { 𝑟 ∈ Ring ∣ { ( 0g ‘ 𝑟 ) } ∈ ( PrmIdeal ‘ 𝑟 ) }