MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  isabl Structured version   Visualization version   GIF version

Theorem isabl 19695
Description: The predicate "is an Abelian (commutative) group". (Contributed by NM, 17-Oct-2011.)
Assertion
Ref Expression
isabl (𝐺 ∈ Abel ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ CMnd))

Proof of Theorem isabl
StepHypRef Expression
1 df-abl 19694 . 2 Abel = (Grp ∩ CMnd)
21elin2 4198 1 (𝐺 ∈ Abel ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ CMnd))
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 394  wcel 2104  Grpcgrp 18857  CMndccmn 19691  Abelcabl 19692
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701
This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-v 3474  df-in 3956  df-abl 19694
This theorem is referenced by:  ablgrp  19696  ablcmn  19698  isabl2  19701  ablpropd  19703  isabld  19706  ghmabl  19743  cntrabl  19754  prdsabld  19773  unitabl  20277  tsmsinv  23874  tgptsmscls  23876  tsmsxplem1  23879  tsmsxplem2  23880  abliso  32462  gicabl  42145  2zrngaabl  46932  pgrpgt2nabl  47132
  Copyright terms: Public domain W3C validator