# Metamath Proof Explorer

## Definition df-mgm

Description: Amagma is a set equipped with an everywhere defined internal operation. Definition 1 in 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 FL, 2-Nov-2009) (Revised by AV, 6-Jan-2020)

Ref Expression
Assertion df-mgm

### Detailed syntax breakdown

Step Hyp Ref Expression
0 cmgm ${class}\mathrm{Mgm}$
1 vg ${setvar}{g}$
2 cbs ${class}\mathrm{Base}$
3 1 cv ${setvar}{g}$
4 3 2 cfv ${class}{\mathrm{Base}}_{{g}}$
5 vb ${setvar}{b}$
6 cplusg ${class}{+}_{𝑔}$
7 3 6 cfv ${class}{+}_{{g}}$
8 vo ${setvar}{o}$
9 vx ${setvar}{x}$
10 5 cv ${setvar}{b}$
11 vy ${setvar}{y}$
12 9 cv ${setvar}{x}$
13 8 cv ${setvar}{o}$
14 11 cv ${setvar}{y}$
15 12 14 13 co ${class}\left({x}{o}{y}\right)$
16 15 10 wcel ${wff}{x}{o}{y}\in {b}$
17 16 11 10 wral ${wff}\forall {y}\in {b}\phantom{\rule{.4em}{0ex}}{x}{o}{y}\in {b}$
18 17 9 10 wral ${wff}\forall {x}\in {b}\phantom{\rule{.4em}{0ex}}\forall {y}\in {b}\phantom{\rule{.4em}{0ex}}{x}{o}{y}\in {b}$
19 18 8 7 wsbc
20 19 5 4 wsbc
21 20 1 cab
22 0 21 wceq