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

Definition df-ablo 20949
Description: Define the class of all Abelian group operations. (Contributed by NM, 2-Nov-2006.) (New usage is discouraged.)
Assertion
Ref Expression
df-ablo  |-  AbelOp  =  {
g  e.  GrpOp  |  A. x  e.  ran  g A. y  e.  ran  g ( x g y )  =  ( y g x ) }
Distinct variable group:    x, g, y

Detailed syntax breakdown of Definition df-ablo
StepHypRef Expression
1 cablo 20948 . 2  class  AbelOp
2 vx . . . . . . . 8  set  x
32cv 1622 . . . . . . 7  class  x
4 vy . . . . . . . 8  set  y
54cv 1622 . . . . . . 7  class  y
6 vg . . . . . . . 8  set  g
76cv 1622 . . . . . . 7  class  g
83, 5, 7co 5858 . . . . . 6  class  ( x g y )
95, 3, 7co 5858 . . . . . 6  class  ( y g x )
108, 9wceq 1623 . . . . 5  wff  ( x g y )  =  ( y g x )
117crn 4690 . . . . 5  class  ran  g
1210, 4, 11wral 2543 . . . 4  wff  A. y  e.  ran  g ( x g y )  =  ( y g x )
1312, 2, 11wral 2543 . . 3  wff  A. x  e.  ran  g A. y  e.  ran  g ( x g y )  =  ( y g x )
14 cgr 20853 . . 3  class  GrpOp
1513, 6, 14crab 2547 . 2  class  { g  e.  GrpOp  |  A. x  e.  ran  g A. y  e.  ran  g ( x g y )  =  ( y g x ) }
161, 15wceq 1623 1  wff  AbelOp  =  {
g  e.  GrpOp  |  A. x  e.  ran  g A. y  e.  ran  g ( x g y )  =  ( y g x ) }
Colors of variables: wff set class
This definition is referenced by:  isablo  20950
  Copyright terms: Public domain W3C validator