Metamath Proof Explorer


Theorem submgmss

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

Ref Expression
Hypothesis submgmss.b 𝐵 = ( Base ‘ 𝑀 )
Assertion submgmss ( 𝑆 ∈ ( SubMgm ‘ 𝑀 ) → 𝑆𝐵 )

Proof

Step Hyp Ref Expression
1 submgmss.b 𝐵 = ( Base ‘ 𝑀 )
2 submgmrcl ( 𝑆 ∈ ( SubMgm ‘ 𝑀 ) → 𝑀 ∈ Mgm )
3 eqid ( 𝑀s 𝑆 ) = ( 𝑀s 𝑆 )
4 1 3 issubmgm2 ( 𝑀 ∈ Mgm → ( 𝑆 ∈ ( SubMgm ‘ 𝑀 ) ↔ ( 𝑆𝐵 ∧ ( 𝑀s 𝑆 ) ∈ Mgm ) ) )
5 2 4 syl ( 𝑆 ∈ ( SubMgm ‘ 𝑀 ) → ( 𝑆 ∈ ( SubMgm ‘ 𝑀 ) ↔ ( 𝑆𝐵 ∧ ( 𝑀s 𝑆 ) ∈ Mgm ) ) )
6 5 ibi ( 𝑆 ∈ ( SubMgm ‘ 𝑀 ) → ( 𝑆𝐵 ∧ ( 𝑀s 𝑆 ) ∈ Mgm ) )
7 6 simpld ( 𝑆 ∈ ( SubMgm ‘ 𝑀 ) → 𝑆𝐵 )