![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > isabl | Structured version Visualization version GIF version |
Description: The predicate "is an Abelian (commutative) group". (Contributed by NM, 17-Oct-2011.) |
Ref | Expression |
---|---|
isabl | ⊢ (𝐺 ∈ Abel ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ CMnd)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-abl 19816 | . 2 ⊢ Abel = (Grp ∩ CMnd) | |
2 | 1 | elin2 4213 | 1 ⊢ (𝐺 ∈ Abel ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ CMnd)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 206 ∧ wa 395 ∈ wcel 2106 Grpcgrp 18964 CMndccmn 19813 Abelcabl 19814 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-8 2108 ax-9 2116 ax-ext 2706 |
This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1540 df-ex 1777 df-sb 2063 df-clab 2713 df-cleq 2727 df-clel 2814 df-v 3480 df-in 3970 df-abl 19816 |
This theorem is referenced by: ablgrp 19818 ablcmn 19820 isabl2 19823 ablpropd 19825 isabld 19828 ghmabl 19865 cntrabl 19876 prdsabld 19895 unitabl 20401 tsmsinv 24172 tgptsmscls 24174 tsmsxplem1 24177 tsmsxplem2 24178 abliso 33024 primrootsunit1 42079 gicabl 43088 2zrngaabl 48094 pgrpgt2nabl 48211 |
Copyright terms: Public domain | W3C validator |