Metamath Proof Explorer


Theorem submgmbas

Description: The base set of a submagma. (Contributed by AV, 26-Feb-2020)

Ref Expression
Hypothesis submgmmgm.h 𝐻 = ( 𝑀s 𝑆 )
Assertion submgmbas ( 𝑆 ∈ ( SubMgm ‘ 𝑀 ) → 𝑆 = ( Base ‘ 𝐻 ) )

Proof

Step Hyp Ref Expression
1 submgmmgm.h 𝐻 = ( 𝑀s 𝑆 )
2 eqid ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
3 2 submgmss ( 𝑆 ∈ ( SubMgm ‘ 𝑀 ) → 𝑆 ⊆ ( Base ‘ 𝑀 ) )
4 1 2 ressbas2 ( 𝑆 ⊆ ( Base ‘ 𝑀 ) → 𝑆 = ( Base ‘ 𝐻 ) )
5 3 4 syl ( 𝑆 ∈ ( SubMgm ‘ 𝑀 ) → 𝑆 = ( Base ‘ 𝐻 ) )