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 e. Smgrp -> G e. Mgm )

Proof

Step Hyp Ref Expression
1 bj-smgrpssmgm 
 |-  Smgrp C_ Mgm
2 1 sseli 
 |-  ( G e. Smgrp -> G e. Mgm )