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

Definition df-ablo 20951
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 20950 . 2  class  AbelOp
2 vx . . . . . . . 8  set  x
32cv 1624 . . . . . . 7  class  x
4 vy . . . . . . . 8  set  y
54cv 1624 . . . . . . 7  class  y
6 vg . . . . . . . 8  set  g
76cv 1624 . . . . . . 7  class  g
83, 5, 7co 5860 . . . . . 6  class  ( x g y )
95, 3, 7co 5860 . . . . . 6  class  ( y g x )
108, 9wceq 1625 . . . . 5  wff  ( x g y )  =  ( y g x )
117crn 4692 . . . . 5  class  ran  g
1210, 4, 11wral 2545 . . . 4  wff  A. y  e.  ran  g ( x g y )  =  ( y g x )
1312, 2, 11wral 2545 . . 3  wff  A. x  e.  ran  g A. y  e.  ran  g ( x g y )  =  ( y g x )
14 cgr 20855 . . 3  class  GrpOp
1513, 6, 14crab 2549 . 2  class  { g  e.  GrpOp  |  A. x  e.  ran  g A. y  e.  ran  g ( x g y )  =  ( y g x ) }
161, 15wceq 1625 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  20952
  Copyright terms: Public domain W3C validator