Users' Mathboxes Mathbox for Jeff Madsen < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-prrngo Unicode version

Definition df-prrngo 26776
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.)
Assertion
Ref Expression
df-prrngo  |-  PrRing  =  {
r  e.  RingOps  |  {
(GId `  ( 1st `  r ) ) }  e.  ( PrIdl `  r
) }

Detailed syntax breakdown of Definition df-prrngo
StepHypRef Expression
1 cprrng 26774 . 2  class  PrRing
2 vr . . . . . . . 8  set  r
32cv 1631 . . . . . . 7  class  r
4 c1st 6136 . . . . . . 7  class  1st
53, 4cfv 5271 . . . . . 6  class  ( 1st `  r )
6 cgi 20870 . . . . . 6  class GId
75, 6cfv 5271 . . . . 5  class  (GId `  ( 1st `  r ) )
87csn 3653 . . . 4  class  { (GId
`  ( 1st `  r
) ) }
9 cpridl 26736 . . . . 5  class  PrIdl
103, 9cfv 5271 . . . 4  class  ( PrIdl `  r )
118, 10wcel 1696 . . 3  wff  { (GId
`  ( 1st `  r
) ) }  e.  ( PrIdl `  r )
12 crngo 21058 . . 3  class  RingOps
1311, 2, 12crab 2560 . 2  class  { r  e.  RingOps  |  { (GId
`  ( 1st `  r
) ) }  e.  ( PrIdl `  r ) }
141, 13wceq 1632 1  wff  PrRing  =  {
r  e.  RingOps  |  {
(GId `  ( 1st `  r ) ) }  e.  ( PrIdl `  r
) }
Colors of variables: wff set class
This definition is referenced by:  isprrngo  26778
  Copyright terms: Public domain W3C validator