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

Theorem isabl 18394
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 18393 . 2 Abel = (Grp ∩ CMnd)
21elin2 4000 1 (𝐺 ∈ Abel ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ CMnd))
Colors of variables: wff setvar class
Syntax hints:  wb 197  wa 384  wcel 2156  Grpcgrp 17623  CMndccmn 18390  Abelcabl 18391
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-v 3393  df-in 3776  df-abl 18393
This theorem is referenced by:  ablgrp  18395  ablcmn  18396  isabl2  18398  ablpropd  18400  isabld  18403  ghmabl  18435  prdsabld  18462  unitabl  18866  tsmsinv  22160  tgptsmscls  22162  tsmsxplem1  22165  tsmsxplem2  22166  abliso  30017  gicabl  38164  2zrngaabl  42506  pgrpgt2nabl  42709
  Copyright terms: Public domain W3C validator