Metamath Proof Explorer

Definition 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 ∈ GrpOp | ∀ x ∈ ran ⁡ g ∀ y ∈ ran ⁡ g x g y = y g x

Detailed syntax breakdown

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 ∀ y ∈ ran ⁡ g x g y = y g x
13 12 3 5 wral wff ∀ x ∈ ran ⁡ g ∀ y ∈ ran ⁡ g x g y = y g x
14 13 1 2 crab class g ∈ GrpOp | ∀ x ∈ ran ⁡ g ∀ y ∈ ran ⁡ g x g y = y g x
15 0 14 wceq wff AbelOp = g ∈ GrpOp | ∀ x ∈ ran ⁡ g ∀ y ∈ ran ⁡ g x g y = y g x