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

Definition df-prrngo 26673
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 26671 . 2  class  PrRing
2 vr . . . . . . . 8  set  r
32cv 1622 . . . . . . 7  class  r
4 c1st 6120 . . . . . . 7  class  1st
53, 4cfv 5255 . . . . . 6  class  ( 1st `  r )
6 cgi 20854 . . . . . 6  class GId
75, 6cfv 5255 . . . . 5  class  (GId `  ( 1st `  r ) )
87csn 3640 . . . 4  class  { (GId
`  ( 1st `  r
) ) }
9 cpridl 26633 . . . . 5  class  PrIdl
103, 9cfv 5255 . . . 4  class  ( PrIdl `  r )
118, 10wcel 1684 . . 3  wff  { (GId
`  ( 1st `  r
) ) }  e.  ( PrIdl `  r )
12 crngo 21042 . . 3  class  RingOps
1311, 2, 12crab 2547 . 2  class  { r  e.  RingOps  |  { (GId
`  ( 1st `  r
) ) }  e.  ( PrIdl `  r ) }
141, 13wceq 1623 1  wff  PrRing  =  {
r  e.  RingOps  |  {
(GId `  ( 1st `  r ) ) }  e.  ( PrIdl `  r
) }
Colors of variables: wff set class
This definition is referenced by:  isprrngo  26675
  Copyright terms: Public domain W3C validator