Theorem sgrpssmgm

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 ⊊ Mgm

Proof

Step	Hyp	Ref	Expression
1		sgrpmgm	⊢ ( 𝑥 ∈ Smgrp → 𝑥 ∈ Mgm )
2	1	ssriv	⊢ Smgrp ⊆ Mgm
3		mgmnsgrpex	⊢ ∃ 𝑥 ∈ Mgm 𝑥 ∉ Smgrp
4		ssexnelpss	⊢ ( ( Smgrp ⊆ Mgm ∧ ∃ 𝑥 ∈ Mgm 𝑥 ∉ Smgrp ) → Smgrp ⊊ Mgm )
5	2 3 4	mp2an	⊢ Smgrp ⊊ Mgm