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

Definition df-ass 20980
Description: A device to add associativity to various sorts of internal operations. The definition is meaningful when  g is a magma at least. (Contributed by FL, 1-Nov-2009.) (New usage is discouraged.)
Assertion
Ref Expression
df-ass  |-  Ass  =  { g  |  A. x  e.  dom  dom  g A. y  e.  dom  dom  g A. z  e. 
dom  dom  g ( ( x g y ) g z )  =  ( x g ( y g z ) ) }
Distinct variable group:    x, g, y, z

Detailed syntax breakdown of Definition df-ass
StepHypRef Expression
1 cass 20979 . 2  class  Ass
2 vx . . . . . . . . . 10  set  x
32cv 1622 . . . . . . . . 9  class  x
4 vy . . . . . . . . . 10  set  y
54cv 1622 . . . . . . . . 9  class  y
6 vg . . . . . . . . . 10  set  g
76cv 1622 . . . . . . . . 9  class  g
83, 5, 7co 5858 . . . . . . . 8  class  ( x g y )
9 vz . . . . . . . . 9  set  z
109cv 1622 . . . . . . . 8  class  z
118, 10, 7co 5858 . . . . . . 7  class  ( ( x g y ) g z )
125, 10, 7co 5858 . . . . . . . 8  class  ( y g z )
133, 12, 7co 5858 . . . . . . 7  class  ( x g ( y g z ) )
1411, 13wceq 1623 . . . . . 6  wff  ( ( x g y ) g z )  =  ( x g ( y g z ) )
157cdm 4689 . . . . . . 7  class  dom  g
1615cdm 4689 . . . . . 6  class  dom  dom  g
1714, 9, 16wral 2543 . . . . 5  wff  A. z  e.  dom  dom  g (
( x g y ) g z )  =  ( x g ( y g z ) )
1817, 4, 16wral 2543 . . . 4  wff  A. y  e.  dom  dom  g A. z  e.  dom  dom  g
( ( x g y ) g z )  =  ( x g ( y g z ) )
1918, 2, 16wral 2543 . . 3  wff  A. x  e.  dom  dom  g A. y  e.  dom  dom  g A. z  e.  dom  dom  g ( ( x g y ) g z )  =  ( x g ( y g z ) )
2019, 6cab 2269 . 2  class  { g  |  A. x  e. 
dom  dom  g A. y  e.  dom  dom  g A. z  e.  dom  dom  g
( ( x g y ) g z )  =  ( x g ( y g z ) ) }
211, 20wceq 1623 1  wff  Ass  =  { g  |  A. x  e.  dom  dom  g A. y  e.  dom  dom  g A. z  e. 
dom  dom  g ( ( x g y ) g z )  =  ( x g ( y g z ) ) }
Colors of variables: wff set class
This definition is referenced by:  isass  20983
  Copyright terms: Public domain W3C validator