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 ∈ SubMgm ⁡ M → S ⊆ B

Proof

Step Hyp Ref Expression
1 submgmss.b ⊢ B = Base M
2 submgmrcl ⊢ S ∈ SubMgm ⁡ M → M ∈ Mgm
3 eqid ⊢ M ↾ 𝑠 S = M ↾ 𝑠 S
4 1 3 issubmgm2 ⊢ M ∈ Mgm → S ∈ SubMgm ⁡ M ↔ S ⊆ B ∧ M ↾ 𝑠 S ∈ Mgm
5 2 4 syl ⊢ S ∈ SubMgm ⁡ M → S ∈ SubMgm ⁡ M ↔ S ⊆ B ∧ M ↾ 𝑠 S ∈ Mgm
6 5 ibi ⊢ S ∈ SubMgm ⁡ M → S ⊆ B ∧ M ↾ 𝑠 S ∈ Mgm
7 6 simpld ⊢ S ∈ SubMgm ⁡ M → S ⊆ B