Metamath Proof Explorer
Description: Monoids are semigroups (elemental version). (Contributed by BJ, 11-Apr-2024) (Proof modification is discouraged.)
|
|
Ref |
Expression |
|
Assertion |
bj-mndsssmgrpel |
Could not format assertion : No typesetting found for |- ( G e. Mnd -> G e. Smgrp ) with typecode |- |
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
bj-mndsssmgrp |
Could not format Mnd C_ Smgrp : No typesetting found for |- Mnd C_ Smgrp with typecode |- |
2 |
1
|
sseli |
Could not format ( G e. Mnd -> G e. Smgrp ) : No typesetting found for |- ( G e. Mnd -> G e. Smgrp ) with typecode |- |