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

Theorem isabl 18977
 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 18976 . 2 Abel = (Grp ∩ CMnd)
21elin2 4102 1 (𝐺 ∈ Abel ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ CMnd))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 209   ∧ wa 399   ∈ wcel 2111  Grpcgrp 18169  CMndccmn 18973  Abelcabl 18974 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729 This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-v 3411  df-in 3865  df-abl 18976 This theorem is referenced by:  ablgrp  18978  ablcmn  18980  isabl2  18982  ablpropd  18984  isabld  18987  ghmabl  19021  cntrabl  19031  prdsabld  19050  unitabl  19489  tsmsinv  22848  tgptsmscls  22850  tsmsxplem1  22853  tsmsxplem2  22854  abliso  30831  gicabl  40416  2zrngaabl  44935  pgrpgt2nabl  45135
 Copyright terms: Public domain W3C validator