Definition df-cmn

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

	Ref	Expression
Assertion	df-cmn	⊢ CMnd = { 𝑔 ∈ Mnd ∣ ∀ 𝑎 ∈ ( Base ‘ 𝑔 ) ∀ 𝑏 ∈ ( Base ‘ 𝑔 ) ( 𝑎 ( +g ‘ 𝑔 ) 𝑏 ) = ( 𝑏 ( +g ‘ 𝑔 ) 𝑎 ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccmn	⊢ CMnd
1		vg	⊢ 𝑔
2		cmnd	⊢ Mnd
3		va	⊢ 𝑎
4		cbs	⊢ Base
5	1	cv	⊢ 𝑔
6	5 4	cfv	⊢ ( Base ‘ 𝑔 )
7		vb	⊢ 𝑏
8	3	cv	⊢ 𝑎
9		cplusg	⊢ +g
10	5 9	cfv	⊢ ( +g ‘ 𝑔 )
11	7	cv	⊢ 𝑏
12	8 11 10	co	⊢ ( 𝑎 ( +g ‘ 𝑔 ) 𝑏 )
13	11 8 10	co	⊢ ( 𝑏 ( +g ‘ 𝑔 ) 𝑎 )
14	12 13	wceq	⊢ ( 𝑎 ( +g ‘ 𝑔 ) 𝑏 ) = ( 𝑏 ( +g ‘ 𝑔 ) 𝑎 )
15	14 7 6	wral	⊢ ∀ 𝑏 ∈ ( Base ‘ 𝑔 ) ( 𝑎 ( +g ‘ 𝑔 ) 𝑏 ) = ( 𝑏 ( +g ‘ 𝑔 ) 𝑎 )
16	15 3 6	wral	⊢ ∀ 𝑎 ∈ ( Base ‘ 𝑔 ) ∀ 𝑏 ∈ ( Base ‘ 𝑔 ) ( 𝑎 ( +g ‘ 𝑔 ) 𝑏 ) = ( 𝑏 ( +g ‘ 𝑔 ) 𝑎 )
17	16 1 2	crab	⊢ { 𝑔 ∈ Mnd ∣ ∀ 𝑎 ∈ ( Base ‘ 𝑔 ) ∀ 𝑏 ∈ ( Base ‘ 𝑔 ) ( 𝑎 ( +g ‘ 𝑔 ) 𝑏 ) = ( 𝑏 ( +g ‘ 𝑔 ) 𝑎 ) }
18	0 17	wceq	⊢ CMnd = { 𝑔 ∈ Mnd ∣ ∀ 𝑎 ∈ ( Base ‘ 𝑔 ) ∀ 𝑏 ∈ ( Base ‘ 𝑔 ) ( 𝑎 ( +g ‘ 𝑔 ) 𝑏 ) = ( 𝑏 ( +g ‘ 𝑔 ) 𝑎 ) }