Metamath Proof Explorer


Theorem bj-smgrpssmgmel

Description: Semigroups are magmas (elemental version). (Contributed by BJ, 12-Apr-2024) (Proof modification is discouraged.)

Ref Expression
Assertion bj-smgrpssmgmel ⊢ G ∈ Smgrp → G ∈ Mgm

Proof

Step Hyp Ref Expression
1 bj-smgrpssmgm ⊢ Smgrp ⊆ Mgm
2 1 sseli ⊢ G ∈ Smgrp → G ∈ Mgm