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

Definition df-ass 21906
 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 21905 . 2
2 vx . . . . . . . . . 10
32cv 1652 . . . . . . . . 9
4 vy . . . . . . . . . 10
54cv 1652 . . . . . . . . 9
6 vg . . . . . . . . . 10
76cv 1652 . . . . . . . . 9
83, 5, 7co 6084 . . . . . . . 8
9 vz . . . . . . . . 9
109cv 1652 . . . . . . . 8
118, 10, 7co 6084 . . . . . . 7
125, 10, 7co 6084 . . . . . . . 8
133, 12, 7co 6084 . . . . . . 7
1411, 13wceq 1653 . . . . . 6
157cdm 4881 . . . . . . 7
1615cdm 4881 . . . . . 6
1714, 9, 16wral 2707 . . . . 5
1817, 4, 16wral 2707 . . . 4
1918, 2, 16wral 2707 . . 3
2019, 6cab 2424 . 2
211, 20wceq 1653 1
 Colors of variables: wff set class This definition is referenced by:  isass  21909
 Copyright terms: Public domain W3C validator