Metamath Proof Explorer

Theorem subgss

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

Ref Expression
Hypothesis issubg.b 
|- B = ( Base ` G )
Assertion subgss 
|- ( S e. ( SubGrp ` G ) -> S C_ B )

Proof

Step Hyp Ref Expression
1 issubg.b 
 |-  B = ( Base ` G )
2 1 issubg 
 |-  ( S e. ( SubGrp ` G ) <-> ( G e. Grp /\ S C_ B /\ ( G |`s S ) e. Grp ) )
3 2 simp2bi 
 |-  ( S e. ( SubGrp ` G ) -> S C_ B )