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

Definition df-com2 21078
Description: A device to add commutativity to various sorts of rings. I use  ran  g because I suppose  g has a neutral element and therefore is onto. (Contributed by FL, 6-Sep-2009.) (New usage is discouraged.)
Assertion
Ref Expression
df-com2  |-  Com2  =  { <. g ,  h >.  |  A. a  e. 
ran  g A. b  e.  ran  g ( a h b )  =  ( b h a ) }
Distinct variable group:    g, h, a, b

Detailed syntax breakdown of Definition df-com2
StepHypRef Expression
1 ccm2 21077 . 2  class  Com2
2 va . . . . . . . 8  set  a
32cv 1622 . . . . . . 7  class  a
4 vb . . . . . . . 8  set  b
54cv 1622 . . . . . . 7  class  b
6 vh . . . . . . . 8  set  h
76cv 1622 . . . . . . 7  class  h
83, 5, 7co 5858 . . . . . 6  class  ( a h b )
95, 3, 7co 5858 . . . . . 6  class  ( b h a )
108, 9wceq 1623 . . . . 5  wff  ( a h b )  =  ( b h a )
11 vg . . . . . . 7  set  g
1211cv 1622 . . . . . 6  class  g
1312crn 4690 . . . . 5  class  ran  g
1410, 4, 13wral 2543 . . . 4  wff  A. b  e.  ran  g ( a h b )  =  ( b h a )
1514, 2, 13wral 2543 . . 3  wff  A. a  e.  ran  g A. b  e.  ran  g ( a h b )  =  ( b h a )
1615, 11, 6copab 4076 . 2  class  { <. g ,  h >.  |  A. a  e.  ran  g A. b  e.  ran  g ( a h b )  =  ( b h a ) }
171, 16wceq 1623 1  wff  Com2  =  { <. g ,  h >.  |  A. a  e. 
ran  g A. b  e.  ran  g ( a h b )  =  ( b h a ) }
Colors of variables: wff set class
This definition is referenced by:  iscom2  21079  com2i  25416
  Copyright terms: Public domain W3C validator