Definition df-ass 32812

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	⊢ Ass = {𝑔 ∣ ∀𝑥 ∈ dom dom 𝑔∀𝑦 ∈ dom dom 𝑔∀𝑧 ∈ dom dom 𝑔((𝑥𝑔𝑦)𝑔𝑧) = (𝑥𝑔(𝑦𝑔𝑧))}

Distinct variable group:   𝑥,𝑔,𝑦,𝑧

Detailed syntax breakdown of Definition df-ass

Step	Hyp	Ref	Expression
1		cass 32811	. 2 class Ass
2		vx	. . . . . . . . . 10 setvar 𝑥
3	2	cv 1474	. . . . . . . . 9 class 𝑥
4		vy	. . . . . . . . . 10 setvar 𝑦
5	4	cv 1474	. . . . . . . . 9 class 𝑦
6		vg	. . . . . . . . . 10 setvar 𝑔
7	6	cv 1474	. . . . . . . . 9 class 𝑔
8	3, 5, 7	co 6549	. . . . . . . 8 class (𝑥𝑔𝑦)
9		vz	. . . . . . . . 9 setvar 𝑧
10	9	cv 1474	. . . . . . . 8 class 𝑧
11	8, 10, 7	co 6549	. . . . . . 7 class ((𝑥𝑔𝑦)𝑔𝑧)
12	5, 10, 7	co 6549	. . . . . . . 8 class (𝑦𝑔𝑧)
13	3, 12, 7	co 6549	. . . . . . 7 class (𝑥𝑔(𝑦𝑔𝑧))
14	11, 13	wceq 1475	. . . . . 6 wff ((𝑥𝑔𝑦)𝑔𝑧) = (𝑥𝑔(𝑦𝑔𝑧))
15	7	cdm 5038	. . . . . . 7 class dom 𝑔
16	15	cdm 5038	. . . . . 6 class dom dom 𝑔
17	14, 9, 16	wral 2896	. . . . 5 wff ∀𝑧 ∈ dom dom 𝑔((𝑥𝑔𝑦)𝑔𝑧) = (𝑥𝑔(𝑦𝑔𝑧))
18	17, 4, 16	wral 2896	. . . 4 wff ∀𝑦 ∈ dom dom 𝑔∀𝑧 ∈ dom dom 𝑔((𝑥𝑔𝑦)𝑔𝑧) = (𝑥𝑔(𝑦𝑔𝑧))
19	18, 2, 16	wral 2896	. . 3 wff ∀𝑥 ∈ dom dom 𝑔∀𝑦 ∈ dom dom 𝑔∀𝑧 ∈ dom dom 𝑔((𝑥𝑔𝑦)𝑔𝑧) = (𝑥𝑔(𝑦𝑔𝑧))
20	19, 6	cab 2596	. 2 class {𝑔 ∣ ∀𝑥 ∈ dom dom 𝑔∀𝑦 ∈ dom dom 𝑔∀𝑧 ∈ dom dom 𝑔((𝑥𝑔𝑦)𝑔𝑧) = (𝑥𝑔(𝑦𝑔𝑧))}
21	1, 20	wceq 1475	1 wff Ass = {𝑔 ∣ ∀𝑥 ∈ dom dom 𝑔∀𝑦 ∈ dom dom 𝑔∀𝑧 ∈ dom dom 𝑔((𝑥𝑔𝑦)𝑔𝑧) = (𝑥𝑔(𝑦𝑔𝑧))}

This definition is referenced by:  isass  32815