Theorem isabl 19713

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

Step	Hyp	Ref	Expression
1		df-abl 19712	. 2 ⊢ Abel = (Grp ∩ CMnd)
2	1	elin2 4155	1 ⊢ (𝐺 ∈ Abel ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ CMnd))

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2113  Grpcgrp 18863  CMndccmn 19709  Abelcabl 19710

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-in 3908  df-abl 19712

This theorem is referenced by:  ablgrp  19714  ablcmn  19716  isabl2  19719  ablpropd  19721  isabld  19724  ghmabl  19761  cntrabl  19772  prdsabld  19791  unitabl  20320  tsmsinv  24092  tgptsmscls  24094  tsmsxplem1  24097  tsmsxplem2  24098  abliso  33118  primrootsunit1  42351  gicabl  43341  2zrngaabl  48496  pgrpgt2nabl  48612