Theorem isabl 19759

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2114  Grpcgrp 18909  CMndccmn 19755  Abelcabl 19756

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-in 3896  df-abl 19758

This theorem is referenced by:  ablgrp  19760  ablcmn  19762  isabl2  19765  ablpropd  19767  isabld  19770  ghmabl  19807  cntrabl  19818  prdsabld  19837  unitabl  20364  tsmsinv  24113  tgptsmscls  24115  tsmsxplem1  24118  tsmsxplem2  24119  abliso  33096  primrootsunit1  42536  gicabl  43527  2zrngaabl  48726  pgrpgt2nabl  48842