Theorem isabl 19750

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

Syntax hints:   ↔ wb 207   ∧ wa 396   ∈ wcel 2119  Grpcgrp 18900  CMndccmn 19746  Abelcabl 19747

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433  df-in 3890  df-abl 19749

This theorem is referenced by:  ablgrp  19751  ablcmn  19753  isabl2  19756  ablpropd  19758  isabld  19761  ghmabl  19798  cntrabl  19809  prdsabld  19828  unitabl  20355  tsmsinv  24131  tgptsmscls  24133  tsmsxplem1  24136  tsmsxplem2  24137  abliso  33115  primrootsunit1  42582  gicabl  43544  2zrngaabl  48741  pgrpgt2nabl  48857