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 \in SubMgm (M) \to S \subseteq B$

Step	Hyp	Ref	Expression
1		submgmss.b	$⊢ B = {Base}_{M}$
2		submgmrcl	$⊢ S \in SubMgm (M) \to M \in Mgm$
3		eqid	$⊢ M ↾_{𝑠} S = M ↾_{𝑠} S$
4	1 3	issubmgm2	$⊢ M \in Mgm \to (S \in SubMgm (M) \leftrightarrow (S \subseteq B \land M ↾_{𝑠} S \in Mgm))$
5	2 4	syl	$⊢ S \in SubMgm (M) \to (S \in SubMgm (M) \leftrightarrow (S \subseteq B \land M ↾_{𝑠} S \in Mgm))$
6	5	ibi	$⊢ S \in SubMgm (M) \to (S \subseteq B \land M ↾_{𝑠} S \in Mgm)$
7	6	simpld	$⊢ S \in SubMgm (M) \to S \subseteq B$

Metamath Proof Explorer