# Metamath Proof Explorer

## 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 ${setvar}{r}$
2 crngo ${class}\mathrm{RingOps}$
3 cgi ${class}\mathrm{GId}$
4 c1st ${class}{1}^{st}$
5 1 cv ${setvar}{r}$
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\}$