Metamath Proof Explorer

Theorem mndsgrp

Description: A monoid is a semigroup. (Contributed by FL, 2-Nov-2009) (Revised by AV, 6-Jan-2020) (Proof shortened by AV, 6-Feb-2020)

Ref Expression
Assertion mndsgrp 
|- ( G e. Mnd -> G e. Smgrp )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Base ` G ) = ( Base ` G )
2 eqid 
 |-  ( +g ` G ) = ( +g ` G )
3 1 2 ismnddef 
 |-  ( G e. Mnd <-> ( G e. Smgrp /\ E. e e. ( Base ` G ) A. x e. ( Base ` G ) ( ( e ( +g ` G ) x ) = x /\ ( x ( +g ` G ) e ) = x ) ) )
4 3 simplbi 
 |-  ( G e. Mnd -> G e. Smgrp )