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

Definition df-ass 26041
 Description: A device to add associativity to various sorts of internal operations. The definition is meaningful when is a magma at least. (Contributed by FL, 1-Nov-2009.) (New usage is discouraged.)
Assertion
Ref Expression
df-ass
Distinct variable group:   ,,,

Detailed syntax breakdown of Definition df-ass
StepHypRef Expression
1 cass 26040 . 2
2 vx . . . . . . . . . 10
32cv 1443 . . . . . . . . 9
4 vy . . . . . . . . . 10
54cv 1443 . . . . . . . . 9
6 vg . . . . . . . . . 10
76cv 1443 . . . . . . . . 9
83, 5, 7co 6290 . . . . . . . 8
9 vz . . . . . . . . 9
109cv 1443 . . . . . . . 8
118, 10, 7co 6290 . . . . . . 7
125, 10, 7co 6290 . . . . . . . 8
133, 12, 7co 6290 . . . . . . 7
1411, 13wceq 1444 . . . . . 6
157cdm 4834 . . . . . . 7
1615cdm 4834 . . . . . 6
1714, 9, 16wral 2737 . . . . 5
1817, 4, 16wral 2737 . . . 4
1918, 2, 16wral 2737 . . 3
2019, 6cab 2437 . 2
211, 20wceq 1444 1
 Colors of variables: wff setvar class This definition is referenced by:  isass  26044
 Copyright terms: Public domain W3C validator