Metamath Proof Explorer


Theorem submgmmgm

Description: Submagmas are themselves magmas under the given operation. (Contributed by AV, 26-Feb-2020)

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

Proof

Step Hyp Ref Expression
1 submgmmgm.h H = M 𝑠 S
2 submgmrcl S SubMgm M M Mgm
3 eqid Base M = Base M
4 3 1 issubmgm2 M Mgm S SubMgm M S Base M H Mgm
5 2 4 syl S SubMgm M S SubMgm M S Base M H Mgm
6 5 ibi S SubMgm M S Base M H Mgm
7 6 simprd S SubMgm M H Mgm