Metamath Proof Explorer


Theorem submgmbas

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

Ref Expression
Hypothesis submgmmgm.h H = M 𝑠 S
Assertion submgmbas S SubMgm M S = Base H

Proof

Step Hyp Ref Expression
1 submgmmgm.h H = M 𝑠 S
2 eqid Base M = Base M
3 2 submgmss S SubMgm M S Base M
4 1 2 ressbas2 S Base M S = Base H
5 3 4 syl S SubMgm M S = Base H