Theorem subgid

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

	Ref	Expression
Hypothesis	issubg.b	|- B = ( Base ` G )
Assertion	subgid	|- ( G e. Grp -> B e. ( SubGrp ` G ) )

Proof

Step	Hyp	Ref	Expression
1		issubg.b	|- B = ( Base ` G )
2		id	|- ( G e. Grp -> G e. Grp )
3		ssidd	|- ( G e. Grp -> B C_ B )
4	1	ressid	|- ( G e. Grp -> ( G |`s B ) = G )
5	4 2	eqeltrd	|- ( G e. Grp -> ( G |`s B ) e. Grp )
6	1	issubg	|- ( B e. ( SubGrp ` G ) <-> ( G e. Grp /\ B C_ B /\ ( G |`s B ) e. Grp ) )
7	2 3 5 6	syl3anbrc	|- ( G e. Grp -> B e. ( SubGrp ` G ) )