Metamath Proof Explorer

Theorem mndbn0

Description: The base set of a monoid is not empty. Statement in Lang p. 3. (Contributed by AV, 29-Dec-2023)

Ref Expression
Hypothesis mndbn0.b B = Base G
Assertion mndbn0 G Mnd B


Step Hyp Ref Expression
1 mndbn0.b B = Base G
2 eqid 0 G = 0 G
3 1 2 mndidcl G Mnd 0 G B
4 3 ne0d G Mnd B