MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-mgm Unicode version

Definition df-mgm 20986
Description: A magma is a binary internal operation. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.)
Assertion
Ref Expression
df-mgm  |-  Magma  =  {
g  |  E. t 
g : ( t  X.  t ) --> t }
Distinct variable group:    t, g

Detailed syntax breakdown of Definition df-mgm
StepHypRef Expression
1 cmagm 20985 . 2  class  Magma
2 vt . . . . . . 7  set  t
32cv 1622 . . . . . 6  class  t
43, 3cxp 4687 . . . . 5  class  ( t  X.  t )
5 vg . . . . . 6  set  g
65cv 1622 . . . . 5  class  g
74, 3, 6wf 5251 . . . 4  wff  g : ( t  X.  t
) --> t
87, 2wex 1528 . . 3  wff  E. t 
g : ( t  X.  t ) --> t
98, 5cab 2269 . 2  class  { g  |  E. t  g : ( t  X.  t ) --> t }
101, 9wceq 1623 1  wff  Magma  =  {
g  |  E. t 
g : ( t  X.  t ) --> t }
Colors of variables: wff set class
This definition is referenced by:  ismgm  20987
  Copyright terms: Public domain W3C validator