Theorem bj-mndsssmgrp

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

	Ref	Expression
Assertion	bj-mndsssmgrp	Could not format assertion : No typesetting found for |- Mnd C_ Smgrp with typecode |-

Proof

Step	Hyp	Ref	Expression
1		df-mnd	Could not format 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 ) } : No typesetting found for |- 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 ) } with typecode |-
2	1	ssrab3	Could not format Mnd C_ Smgrp : No typesetting found for |- Mnd C_ Smgrp with typecode |-