Theorem isabl 19704

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 19703	. 2 ⊢ Abel = (Grp ∩ CMnd)
2	1	elin2 4152	1 ⊢ (𝐺 ∈ Abel ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ CMnd))

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2113  Grpcgrp 18854  CMndccmn 19700  Abelcabl 19701

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 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-v 3439  df-in 3905  df-abl 19703

This theorem is referenced by:  ablgrp  19705  ablcmn  19707  isabl2  19710  ablpropd  19712  isabld  19715  ghmabl  19752  cntrabl  19763  prdsabld  19782  unitabl  20311  tsmsinv  24083  tgptsmscls  24085  tsmsxplem1  24088  tsmsxplem2  24089  abliso  33046  primrootsunit1  42263  gicabl  43256  2zrngaabl  48412  pgrpgt2nabl  48528