This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-cmn

Description: Define class of all commutative monoids. (Contributed by Mario Carneiro, 6-Jan-2015)

Ref Expression
Assertion df-cmn ⊢ CMnd = g ∈ Mnd | ∀ a ∈ Base g ∀ b ∈ Base g a + g b = b + g a

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccmn class CMnd
1 vg setvar g
2 cmnd class Mnd
3 va setvar a
4 cbs class Base
5 1 cv setvar g
6 5 4 cfv class Base g
7 vb setvar b
8 3 cv setvar a
9 cplusg class + 𝑔
10 5 9 cfv class + g
11 7 cv setvar b
12 8 11 10 co class a + g b
13 11 8 10 co class b + g a
14 12 13 wceq wff a + g b = b + g a
15 14 7 6 wral wff ∀ b ∈ Base g a + g b = b + g a
16 15 3 6 wral wff ∀ a ∈ Base g ∀ b ∈ Base g a + g b = b + g a
17 16 1 2 crab class g ∈ Mnd | ∀ a ∈ Base g ∀ b ∈ Base g a + g b = b + g a
18 0 17 wceq wff CMnd = g ∈ Mnd | ∀ a ∈ Base g ∀ b ∈ Base g a + g b = b + g a