Metamath Proof Explorer


Theorem subgid

Description: A group is a subgroup of itself. (Contributed by Mario Carneiro, 7-Dec-2014)

Ref Expression
Hypothesis issubg.b B=BaseG
Assertion subgid GGrpBSubGrpG

Proof

Step Hyp Ref Expression
1 issubg.b B=BaseG
2 id GGrpGGrp
3 ssidd GGrpBB
4 1 ressid GGrpG𝑠B=G
5 4 2 eqeltrd GGrpG𝑠BGrp
6 1 issubg BSubGrpGGGrpBBG𝑠BGrp
7 2 3 5 6 syl3anbrc GGrpBSubGrpG