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

Metamath Proof Explorer

Theorem subggrp

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

		Ref	Expression
	Hypothesis	subggrp.h	$⊢ H = G ↾_{𝑠} S$
	Assertion	subggrp	$⊢ S \in SubGrp (G) \to H \in Grp$

Step	Hyp	Ref	Expression
1		subggrp.h	$⊢ H = G ↾_{𝑠} S$
2		eqid	$⊢ {Base}_{G} = {Base}_{G}$
3	2	issubg	$⊢ S \in SubGrp (G) \leftrightarrow (G \in Grp \land S \subseteq {Base}_{G} \land G ↾_{𝑠} S \in Grp)$
4	3	simp3bi	$⊢ S \in SubGrp (G) \to G ↾_{𝑠} S \in Grp$
5	1 4	eqeltrid	$⊢ S \in SubGrp (G) \to H \in Grp$