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

Theorem isabl 19803
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 19802 . 2 Abel = (Grp ∩ CMnd)
21elin2 4202 1 (𝐺 ∈ Abel ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ CMnd))
Colors of variables: wff setvar class
Syntax hints:  wb 206  wa 395  wcel 2107  Grpcgrp 18952  CMndccmn 19799  Abelcabl 19800
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-v 3481  df-in 3957  df-abl 19802
This theorem is referenced by:  ablgrp  19804  ablcmn  19806  isabl2  19809  ablpropd  19811  isabld  19814  ghmabl  19851  cntrabl  19862  prdsabld  19881  unitabl  20385  tsmsinv  24157  tgptsmscls  24159  tsmsxplem1  24162  tsmsxplem2  24163  abliso  33042  primrootsunit1  42099  gicabl  43116  2zrngaabl  48171  pgrpgt2nabl  48287
  Copyright terms: Public domain W3C validator