Theorem bj-mndsssmgrp

Description: Monoids are semigroups. (Contributed by BJ, 11-Apr-2024) (Proof modification is discouraged.)

	Ref	Expression
Assertion	bj-mndsssmgrp	$$⊢\mathrm{Mnd}\subseteq \mathrm{Smgrp}$$

Proof

Step	Hyp	Ref	Expression
1		df-mnd	$$⊢\mathrm{Mnd}=\left\{g\in \mathrm{Smgrp}|\underset{\dot{}}{[}{\mathrm{Base}}_g/b\underset{\dot{}}{]}\underset{\dot{}}{[}{+}_g/p\underset{\dot{}}{]}\exists e\in b\forall x\in b\left(epx=x\wedge xpe=x\right)\right\}$$
2	1	ssrab3	$$⊢\mathrm{Mnd}\subseteq \mathrm{Smgrp}$$