Description: Every subgroup of an abelian group is normal. (Contributed by Mario Carneiro, 14-Jun-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | ablnsg | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid | |
|
2 | eqid | |
|
3 | 1 2 | ablcom | |
4 | 3 | 3expb | |
5 | 4 | eleq1d | |
6 | 5 | ralrimivva | |
7 | 1 2 | isnsg | |
8 | 7 | rbaib | |
9 | 6 8 | syl | |
10 | 9 | eqrdv | |