Metamath Proof Explorer

Theorem bj-mndsssmgrp

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

Ref Expression
Assertion bj-mndsssmgrp 
|- Mnd C_ Smgrp

Proof

Step Hyp Ref Expression
1 df-mnd 
 |-  Mnd = { g e. Smgrp | [. ( Base ` g ) / b ]. [. ( +g ` g ) / p ]. E. e e. b A. x e. b ( ( e p x ) = x /\ ( x p e ) = x ) }
2 1 ssrab3 
 |-  Mnd C_ Smgrp