Metamath Proof Explorer


Theorem submgmss

Description: Submagmas are subsets of the base set. (Contributed by AV, 26-Feb-2020)

Ref Expression
Hypothesis submgmss.b
|- B = ( Base ` M )
Assertion submgmss
|- ( S e. ( SubMgm ` M ) -> S C_ B )

Proof

Step Hyp Ref Expression
1 submgmss.b
 |-  B = ( Base ` M )
2 submgmrcl
 |-  ( S e. ( SubMgm ` M ) -> M e. Mgm )
3 eqid
 |-  ( M |`s S ) = ( M |`s S )
4 1 3 issubmgm2
 |-  ( M e. Mgm -> ( S e. ( SubMgm ` M ) <-> ( S C_ B /\ ( M |`s S ) e. Mgm ) ) )
5 2 4 syl
 |-  ( S e. ( SubMgm ` M ) -> ( S e. ( SubMgm ` M ) <-> ( S C_ B /\ ( M |`s S ) e. Mgm ) ) )
6 5 ibi
 |-  ( S e. ( SubMgm ` M ) -> ( S C_ B /\ ( M |`s S ) e. Mgm ) )
7 6 simpld
 |-  ( S e. ( SubMgm ` M ) -> S C_ B )