Description: Obsolete version of dfmgm as of 3Feb2020. A magma is a binary internal operation. (Contributed by FL, 2Nov2009) (New usage is discouraged.)
Ref  Expression  

Assertion  dfmgmOLD   Magma = { g  E. t g : ( t X. t ) > t } 
Step  Hyp  Ref  Expression 

0  cmagm   Magma 

1  vg   g 

2  vt   t 

3  1  cv   g 
4  2  cv   t 
5  4 4  cxp   ( t X. t ) 
6  5 4 3  wf   g : ( t X. t ) > t 
7  6 2  wex   E. t g : ( t X. t ) > t 
8  7 1  cab   { g  E. t g : ( t X. t ) > t } 
9  0 8  wceq   Magma = { g  E. t g : ( t X. t ) > t } 