Description: The class of all semigroups is a proper subclass of the class of all magmas. (Contributed by AV, 29-Jan-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | sgrpssmgm | |- Smgrp C. Mgm |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sgrpmgm | |- ( x e. Smgrp -> x e. Mgm ) |
|
2 | 1 | ssriv | |- Smgrp C_ Mgm |
3 | mgmnsgrpex | |- E. x e. Mgm x e/ Smgrp |
|
4 | ssexnelpss | |- ( ( Smgrp C_ Mgm /\ E. x e. Mgm x e/ Smgrp ) -> Smgrp C. Mgm ) |
|
5 | 2 3 4 | mp2an | |- Smgrp C. Mgm |