This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem subgss

Description: A subgroup is a subset. (Contributed by Mario Carneiro, 2-Dec-2014)

		Ref	Expression
	Hypothesis	issubg.b	$⊢ B = {Base}_{G}$
	Assertion	subgss	$⊢ S \in SubGrp (G) \to S \subseteq B$

Step	Hyp	Ref	Expression
1		issubg.b	$⊢ B = {Base}_{G}$
2	1	issubg	$⊢ S \in SubGrp (G) \leftrightarrow (G \in Grp \land S \subseteq B \land G ↾_{𝑠} S \in Grp)$
3	2	simp2bi	$⊢ S \in SubGrp (G) \to S \subseteq B$