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 ( 𝐺 ∈ Smgrp → 𝐺 ∈ Mgm )

Proof

Step Hyp Ref Expression
1 bj-smgrpssmgm Smgrp ⊆ Mgm
2 1 sseli ( 𝐺 ∈ Smgrp → 𝐺 ∈ Mgm )