Theorem isabl 19371

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

Syntax hints:   ↔ wb 205   ∧ wa 395   ∈ wcel 2109  Grpcgrp 18558  CMndccmn 19367  Abelcabl 19368

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1544  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3432  df-in 3898  df-abl 19370

This theorem is referenced by:  ablgrp  19372  ablcmn  19374  isabl2  19376  ablpropd  19378  isabld  19381  ghmabl  19415  cntrabl  19425  prdsabld  19444  unitabl  19891  tsmsinv  23280  tgptsmscls  23282  tsmsxplem1  23285  tsmsxplem2  23286  abliso  31284  gicabl  40904  2zrngaabl  45454  pgrpgt2nabl  45654