Metamath Proof Explorer


Theorem subgss

Description: A subgroup is a subset. (Contributed by Mario Carneiro, 2-Dec-2014)

Ref Expression
Hypothesis issubg.b B=BaseG
Assertion subgss SSubGrpGSB

Proof

Step Hyp Ref Expression
1 issubg.b B=BaseG
2 1 issubg SSubGrpGGGrpSBG𝑠SGrp
3 2 simp2bi SSubGrpGSB