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	Could not format assertion : No typesetting found for |- PrmRing = { r e. Ring | { ( 0g ` r ) } e. ( PrmIdeal ` r ) } with typecode |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cprmrng	Could not format PrmRing : No typesetting found for class PrmRing with typecode class
1		vr	$$setvarr$$
2		crg	$$class\mathrm{Ring}$$
3		c0g	$$class{0}_{𝑔}$$
4	1	cv	$$setvarr$$
5	4 3	cfv	$$class{0}_r$$
6	5	csn	$$class\left\{0_r\right\}$$
7		cprmidl	$$class\mathrm{PrmIdeal}$$
8	4 7	cfv	$$class\mathrm{PrmIdeal}\left(r\right)$$
9	6 8	wcel	$$wff\left\{0_r\right\}\in \mathrm{PrmIdeal}\left(r\right)$$
10	9 1 2	crab	$$class\left\{r\in \mathrm{Ring}|\left\{0_r\right\}\in \mathrm{PrmIdeal}\left(r\right)\right\}$$
11	0 10	wceq	Could not format PrmRing = { r e. Ring | { ( 0g ` r ) } e. ( PrmIdeal ` r ) } : No typesetting found for wff PrmRing = { r e. Ring | { ( 0g ` r ) } e. ( PrmIdeal ` r ) } with typecode wff