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

Theorem isabl 18642
 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 18641 . 2 Abel = (Grp ∩ CMnd)
21elin2 4099 1 (𝐺 ∈ Abel ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ CMnd))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 207   ∧ wa 396   ∈ wcel 2081  Grpcgrp 17866  CMndccmn 18638  Abelcabl 18639 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-ext 2769 This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-v 3439  df-in 3870  df-abl 18641 This theorem is referenced by:  ablgrp  18643  ablcmn  18644  isabl2  18646  ablpropd  18648  isabld  18651  ghmabl  18683  prdsabld  18710  unitabl  19113  tsmsinv  22444  tgptsmscls  22446  tsmsxplem1  22449  tsmsxplem2  22450  abliso  30362  cntrabl  30514  gicabl  39209  2zrngaabl  43719  pgrpgt2nabl  43920
 Copyright terms: Public domain W3C validator