Definition df-ablo 28626

Description: Define the class of all Abelian group operations. (Contributed by NM, 2-Nov-2006.) (New usage is discouraged.)

Assertion

Ref	Expression
df-ablo	⊢ AbelOp = {𝑔 ∈ GrpOp ∣ ∀𝑥 ∈ ran 𝑔∀𝑦 ∈ ran 𝑔(𝑥𝑔𝑦) = (𝑦𝑔𝑥)}

Distinct variable group:   𝑥,𝑔,𝑦

Detailed syntax breakdown of Definition df-ablo

Step	Hyp	Ref	Expression
1		cablo 28625	. 2 class AbelOp
2		vx	. . . . . . . 8 setvar 𝑥
3	2	cv 1542	. . . . . . 7 class 𝑥
4		vy	. . . . . . . 8 setvar 𝑦
5	4	cv 1542	. . . . . . 7 class 𝑦
6		vg	. . . . . . . 8 setvar 𝑔
7	6	cv 1542	. . . . . . 7 class 𝑔
8	3, 5, 7	co 7213	. . . . . 6 class (𝑥𝑔𝑦)
9	5, 3, 7	co 7213	. . . . . 6 class (𝑦𝑔𝑥)
10	8, 9	wceq 1543	. . . . 5 wff (𝑥𝑔𝑦) = (𝑦𝑔𝑥)
11	7	crn 5552	. . . . 5 class ran 𝑔
12	10, 4, 11	wral 3061	. . . 4 wff ∀𝑦 ∈ ran 𝑔(𝑥𝑔𝑦) = (𝑦𝑔𝑥)
13	12, 2, 11	wral 3061	. . 3 wff ∀𝑥 ∈ ran 𝑔∀𝑦 ∈ ran 𝑔(𝑥𝑔𝑦) = (𝑦𝑔𝑥)
14		cgr 28570	. . 3 class GrpOp
15	13, 6, 14	crab 3065	. 2 class {𝑔 ∈ GrpOp ∣ ∀𝑥 ∈ ran 𝑔∀𝑦 ∈ ran 𝑔(𝑥𝑔𝑦) = (𝑦𝑔𝑥)}
16	1, 15	wceq 1543	1 wff AbelOp = {𝑔 ∈ GrpOp ∣ ∀𝑥 ∈ ran 𝑔∀𝑦 ∈ ran 𝑔(𝑥𝑔𝑦) = (𝑦𝑔𝑥)}

This definition is referenced by:  isablo  28627