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

Definition df-risc 26717
Description: Define the ring isomorphism relation. (Contributed by Jeff Madsen, 16-Jun-2011.)
Assertion
Ref Expression
df-risc  |-  ~=r  =  { <. r ,  s
>.  |  ( (
r  e.  RingOps  /\  s  e.  RingOps )  /\  E. f  f  e.  (
r  RngIso  s ) ) }
Distinct variable group:    s, r, f

Detailed syntax breakdown of Definition df-risc
StepHypRef Expression
1 crisc 26696 . 2  class  ~=r
2 vr . . . . . . 7  set  r
32cv 1631 . . . . . 6  class  r
4 crngo 21058 . . . . . 6  class  RingOps
53, 4wcel 1696 . . . . 5  wff  r  e.  RingOps
6 vs . . . . . . 7  set  s
76cv 1631 . . . . . 6  class  s
87, 4wcel 1696 . . . . 5  wff  s  e.  RingOps
95, 8wa 358 . . . 4  wff  ( r  e.  RingOps  /\  s  e.  RingOps )
10 vf . . . . . . 7  set  f
1110cv 1631 . . . . . 6  class  f
12 crngiso 26695 . . . . . . 7  class  RngIso
133, 7, 12co 5874 . . . . . 6  class  ( r 
RngIso  s )
1411, 13wcel 1696 . . . . 5  wff  f  e.  ( r  RngIso  s )
1514, 10wex 1531 . . . 4  wff  E. f 
f  e.  ( r 
RngIso  s )
169, 15wa 358 . . 3  wff  ( ( r  e.  RingOps  /\  s  e.  RingOps )  /\  E. f  f  e.  (
r  RngIso  s ) )
1716, 2, 6copab 4092 . 2  class  { <. r ,  s >.  |  ( ( r  e.  RingOps  /\  s  e.  RingOps )  /\  E. f  f  e.  ( r  RngIso  s ) ) }
181, 17wceq 1632 1  wff  ~=r  =  { <. r ,  s
>.  |  ( (
r  e.  RingOps  /\  s  e.  RingOps )  /\  E. f  f  e.  (
r  RngIso  s ) ) }
Colors of variables: wff set class
This definition is referenced by:  isriscg  26718  riscer  26722
  Copyright terms: Public domain W3C validator