Description: A group is a subgroup of itself. (Contributed by Mario Carneiro, 7-Dec-2014)
Ref | Expression | ||
---|---|---|---|
Hypothesis | issubg.b | |
|
Assertion | subgid | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | issubg.b | |
|
2 | id | |
|
3 | ssidd | |
|
4 | 1 | ressid | |
5 | 4 2 | eqeltrd | |
6 | 1 | issubg | |
7 | 2 3 5 6 | syl3anbrc | |