Definition df-ass 33642

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

Step	Hyp	Ref	Expression
1		cass 33641	. 2 class Ass
2		vx	. . . . . . . . . 10 setvar x
3	2	cv 1482	. . . . . . . . 9 class x
4		vy	. . . . . . . . . 10 setvar y
5	4	cv 1482	. . . . . . . . 9 class y
6		vg	. . . . . . . . . 10 setvar g
7	6	cv 1482	. . . . . . . . 9 class g
8	3, 5, 7	co 6650	. . . . . . . 8 class ( x g y )
9		vz	. . . . . . . . 9 setvar z
10	9	cv 1482	. . . . . . . 8 class z
11	8, 10, 7	co 6650	. . . . . . 7 class ( ( x g y ) g z )
12	5, 10, 7	co 6650	. . . . . . . 8 class ( y g z )
13	3, 12, 7	co 6650	. . . . . . 7 class ( x g ( y g z ) )
14	11, 13	wceq 1483	. . . . . 6 wff ( ( x g y ) g z ) = ( x g ( y g z ) )
15	7	cdm 5114	. . . . . . 7 class dom g
16	15	cdm 5114	. . . . . 6 class dom dom g
17	14, 9, 16	wral 2912	. . . . 5 wff A. z e. dom dom g ( ( x g y ) g z ) = ( x g ( y g z ) )
18	17, 4, 16	wral 2912	. . . 4 wff A. y e. dom dom g A. z e. dom dom g ( ( x g y ) g z ) = ( x g ( y g z ) )
19	18, 2, 16	wral 2912	. . 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 ) )
20	19, 6	cab 2608	. 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 ) ) }
21	1, 20	wceq 1483	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 ) ) }

This definition is referenced by:  isass  33645