Theorem bj-grpssmnd

Description: Groups are monoids. (Contributed by BJ, 5-Jan-2024) (Proof modification is discouraged.)

	Ref	Expression
Assertion	bj-grpssmnd	$$⊢\mathrm{Grp}\subseteq \mathrm{Mnd}$$

Proof

Step	Hyp	Ref	Expression
1		df-grp	$$⊢\mathrm{Grp}=\left\{x\in \mathrm{Mnd}|\forall y\in {\mathrm{Base}}_x\exists z\in {\mathrm{Base}}_{x}z{+}_{x}y=0_x\right\}$$
2	1	ssrab3	$$⊢\mathrm{Grp}\subseteq \mathrm{Mnd}$$