df-ablo

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

		Ref	Expression
	Assertion	df-ablo	$⊢ AbelOp = \{g \in GrpOp \| \forall x \in ran g \forall y \in ran g x g y = y g x\}$

Step	Hyp	Ref	Expression
0		cablo	$class AbelOp$
1		vg	$setvar g$
2		cgr	$class GrpOp$
3		vx	$setvar x$
4	1	cv	$setvar g$
5	4	crn	$class ran g$
6		vy	$setvar y$
7	3	cv	$setvar x$
8	6	cv	$setvar y$
9	7 8 4	co	$class (x g y)$
10	8 7 4	co	$class (y g x)$
11	9 10	wceq	$wff x g y = y g x$
12	11 6 5	wral	$wff \forall y \in ran g x g y = y g x$
13	12 3 5	wral	$wff \forall x \in ran g \forall y \in ran g x g y = y g x$
14	13 1 2	crab	$class \{g \in GrpOp \| \forall x \in ran g \forall y \in ran g x g y = y g x\}$
15	0 14	wceq	$wff AbelOp = \{g \in GrpOp \| \forall x \in ran g \forall y \in ran g x g y = y g x\}$

Metamath Proof Explorer