Theorem nsgsubg

Description: A normal subgroup is a subgroup. (Contributed by Mario Carneiro, 18-Jan-2015)

	Ref	Expression
Assertion	nsgsubg	|- ( S e. ( NrmSGrp ` G ) -> S e. ( SubGrp ` G ) )

Proof

Step	Hyp	Ref	Expression
1		eqid	|- ( Base ` G ) = ( Base ` G )
2		eqid	|- ( +g ` G ) = ( +g ` G )
3	1 2	isnsg	|- ( S e. ( NrmSGrp ` G ) <-> ( S e. ( SubGrp ` G ) /\ A. x e. ( Base ` G ) A. y e. ( Base ` G ) ( ( x ( +g ` G ) y ) e. S <-> ( y ( +g ` G ) x ) e. S ) ) )
4	3	simplbi	|- ( S e. ( NrmSGrp ` G ) -> S e. ( SubGrp ` G ) )