Users' Mathboxes Mathbox for Jeff Madsen < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-mgmOLD Structured version   Visualization version   GIF version

Definition df-mgmOLD 32818
Description: Obsolete version of df-mgm 17065 as of 3-Feb-2020. A magma is a binary internal operation. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.)
Assertion
Ref Expression
df-mgmOLD Magma = {𝑔 ∣ ∃𝑡 𝑔:(𝑡 × 𝑡)⟶𝑡}
Distinct variable group:   𝑡,𝑔

Detailed syntax breakdown of Definition df-mgmOLD
StepHypRef Expression
1 cmagm 32817 . 2 class Magma
2 vt . . . . . . 7 setvar 𝑡
32cv 1474 . . . . . 6 class 𝑡
43, 3cxp 5036 . . . . 5 class (𝑡 × 𝑡)
5 vg . . . . . 6 setvar 𝑔
65cv 1474 . . . . 5 class 𝑔
74, 3, 6wf 5800 . . . 4 wff 𝑔:(𝑡 × 𝑡)⟶𝑡
87, 2wex 1695 . . 3 wff 𝑡 𝑔:(𝑡 × 𝑡)⟶𝑡
98, 5cab 2596 . 2 class {𝑔 ∣ ∃𝑡 𝑔:(𝑡 × 𝑡)⟶𝑡}
101, 9wceq 1475 1 wff Magma = {𝑔 ∣ ∃𝑡 𝑔:(𝑡 × 𝑡)⟶𝑡}
Colors of variables: wff setvar class
This definition is referenced by:  ismgmOLD  32819
  Copyright terms: Public domain W3C validator