Theorem bj-grpssmnd

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

	Ref	Expression
Assertion	bj-grpssmnd	⊢ Grp ⊆ Mnd

Proof

Step	Hyp	Ref	Expression
1		df-grp	⊢ Grp = { 𝑥 ∈ Mnd ∣ ∀ 𝑦 ∈ ( Base ‘ 𝑥 ) ∃ 𝑧 ∈ ( Base ‘ 𝑥 ) ( 𝑧 ( +g ‘ 𝑥 ) 𝑦 ) = ( 0g ‘ 𝑥 ) }
2	1	ssrab3	⊢ Grp ⊆ Mnd