Definition df-mgm2

Description: Amagma is a set equipped with a closed operation. Definition 1 of BourbakiAlg1 p. 1, or definition of a groupoid in section I.1 of Bruck p. 1. Note: The term "groupoid" is now widely used to refer to other objects: (small) categories all of whose morphisms are invertible, or groups with a partial function replacing the binary operation. Therefore, we will only use the term "magma" for the present notion in set.mm. (Contributed by AV, 6-Jan-2020)

	Ref	Expression
Assertion	df-mgm2	⊢ MgmALT = { 𝑚 ∣ ( +g ‘ 𝑚 ) clLaw ( Base ‘ 𝑚 ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmgm2	⊢ MgmALT
1		vm	⊢ 𝑚
2		cplusg	⊢ +g
3	1	cv	⊢ 𝑚
4	3 2	cfv	⊢ ( +g ‘ 𝑚 )
5		ccllaw	⊢ clLaw
6		cbs	⊢ Base
7	3 6	cfv	⊢ ( Base ‘ 𝑚 )
8	4 7 5	wbr	⊢ ( +g ‘ 𝑚 ) clLaw ( Base ‘ 𝑚 )
9	8 1	cab	⊢ { 𝑚 ∣ ( +g ‘ 𝑚 ) clLaw ( Base ‘ 𝑚 ) }
10	0 9	wceq	⊢ MgmALT = { 𝑚 ∣ ( +g ‘ 𝑚 ) clLaw ( Base ‘ 𝑚 ) }