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	$$⊢\mathrm{PrRing}=\left\{r\in \mathrm{RingOps}|\left\{\mathrm{GId}\left(1^{st}\left(r\right)\right)\right\}\in \mathrm{PrIdl}\left(r\right)\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cprrng	$$class\mathrm{PrRing}$$
1		vr	$$setvarr$$
2		crngo	$$class\mathrm{RingOps}$$
3		cgi	$$class\mathrm{GId}$$
4		c1st	$$class{1}^{st}$$
5	1	cv	$$setvarr$$
6	5 4	cfv	$$class{1}^{st}\left(r\right)$$
7	6 3	cfv	$$class\mathrm{GId}\left(1^{st}\left(r\right)\right)$$
8	7	csn	$$class\left\{\mathrm{GId}\left(1^{st}\left(r\right)\right)\right\}$$
9		cpridl	$$class\mathrm{PrIdl}$$
10	5 9	cfv	$$class\mathrm{PrIdl}\left(r\right)$$
11	8 10	wcel	$$wff\left\{\mathrm{GId}\left(1^{st}\left(r\right)\right)\right\}\in \mathrm{PrIdl}\left(r\right)$$
12	11 1 2	crab	$$class\left\{r\in \mathrm{RingOps}|\left\{\mathrm{GId}\left(1^{st}\left(r\right)\right)\right\}\in \mathrm{PrIdl}\left(r\right)\right\}$$
13	0 12	wceq	$$wff\mathrm{PrRing}=\left\{r\in \mathrm{RingOps}|\left\{\mathrm{GId}\left(1^{st}\left(r\right)\right)\right\}\in \mathrm{PrIdl}\left(r\right)\right\}$$