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

Definition df-risc 26866
Description: Define the ring isomorphism relation. (Contributed by Jeff Madsen, 16-Jun-2011.)
Assertion
Ref Expression
df-risc
Distinct variable group:   , ,

Detailed syntax breakdown of Definition df-risc
StepHypRef Expression
1 crisc 26845 . 2
2 vr . . . . . . 7
32cv 1653 . . . . . 6
4 crngo 21999 . . . . . 6
53, 4wcel 1728 . . . . 5
6 vs . . . . . . 7
76cv 1653 . . . . . 6
87, 4wcel 1728 . . . . 5
95, 8wa 360 . . . 4
10 vf . . . . . . 7
1110cv 1653 . . . . . 6
12 crngiso 26844 . . . . . . 7
133, 7, 12co 6133 . . . . . 6
1411, 13wcel 1728 . . . . 5
1514, 10wex 1551 . . . 4
169, 15wa 360 . . 3
1716, 2, 6copab 4304 . 2
181, 17wceq 1654 1
Colors of variables: wff set class
This definition is referenced by:  isriscg  26867  riscer  26871
  Copyright terms: Public domain W3C validator