Theorem submgmbas

Description: The base set of a submagma. (Contributed by AV, 26-Feb-2020)

	Ref	Expression
Hypothesis	submgmmgm.h	|- H = ( M |`s S )
Assertion	submgmbas	|- ( S e. ( SubMgm ` M ) -> S = ( Base ` H ) )

Proof

Step	Hyp	Ref	Expression
1		submgmmgm.h	|- H = ( M |`s S )
2		eqid	|- ( Base ` M ) = ( Base ` M )
3	2	submgmss	|- ( S e. ( SubMgm ` M ) -> S C_ ( Base ` M ) )
4	1 2	ressbas2	|- ( S C_ ( Base ` M ) -> S = ( Base ` H ) )
5	3 4	syl	|- ( S e. ( SubMgm ` M ) -> S = ( Base ` H ) )