MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-starv Unicode version

Definition df-starv 13223
Description: Define the involution function of a *-ring. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.)
Assertion
Ref Expression
df-starv  |-  * r  = Slot  4

Detailed syntax breakdown of Definition df-starv
StepHypRef Expression
1 cstv 13210 . 2  class  * r
2 c4 9797 . . 3  class  4
32cslot 13147 . 2  class Slot  4
41, 3wceq 1623 1  wff  * r  = Slot  4
Colors of variables: wff set class
This definition is referenced by:  starvndx  13259  starvid  13260  ressstarv  13262
  Copyright terms: Public domain W3C validator