Theorem isabl 19754

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

Syntax hints:   ↔ wb 208   ∧ wa 397   ∈ wcel 2121  Grpcgrp 18904  CMndccmn 19750  Abelcabl 19751

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-tru 1551  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-v 3435  df-in 3892  df-abl 19753

This theorem is referenced by:  ablgrp  19755  ablcmn  19757  isabl2  19760  ablpropd  19762  isabld  19765  ghmabl  19802  cntrabl  19813  prdsabld  19832  unitabl  20359  tsmsinv  24135  tgptsmscls  24137  tsmsxplem1  24140  tsmsxplem2  24141  abliso  33119  primrootsunit1  42597  gicabl  43559  2zrngaabl  48755  pgrpgt2nabl  48871