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

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

Metamath Proof Explorer