Metamath Proof Explorer

Definition df-ass

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.)

Ref Expression
Assertion df-ass ⊢ Ass = g | ∀ x ∈ dom ⁡ dom ⁡ g ∀ y ∈ dom ⁡ dom ⁡ g ∀ z ∈ dom ⁡ dom ⁡ g x g y g z = x g y g z

Detailed syntax breakdown

Step Hyp Ref Expression
0 cass class Ass
1 vg setvar g
2 vx setvar x
3 1 cv setvar g
4 3 cdm class dom ⁡ g
5 4 cdm class dom ⁡ dom ⁡ g
6 vy setvar y
7 vz setvar z
8 2 cv setvar x
9 6 cv setvar y
10 8 9 3 co class x g y
11 7 cv setvar z
12 10 11 3 co class x g y g z
13 9 11 3 co class y g z
14 8 13 3 co class x g y g z
15 12 14 wceq wff x g y g z = x g y g z
16 15 7 5 wral wff ∀ z ∈ dom ⁡ dom ⁡ g x g y g z = x g y g z
17 16 6 5 wral wff ∀ y ∈ dom ⁡ dom ⁡ g ∀ z ∈ dom ⁡ dom ⁡ g x g y g z = x g y g z
18 17 2 5 wral wff ∀ x ∈ dom ⁡ dom ⁡ g ∀ y ∈ dom ⁡ dom ⁡ g ∀ z ∈ dom ⁡ dom ⁡ g x g y g z = x g y g z
19 18 1 cab class g | ∀ x ∈ dom ⁡ dom ⁡ g ∀ y ∈ dom ⁡ dom ⁡ g ∀ z ∈ dom ⁡ dom ⁡ g x g y g z = x g y g z
20 0 19 wceq wff Ass = g | ∀ x ∈ dom ⁡ dom ⁡ g ∀ y ∈ dom ⁡ dom ⁡ g ∀ z ∈ dom ⁡ dom ⁡ g x g y g z = x g y g z