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 e. Mnd -> B =/= (/) )

Proof

Step Hyp Ref Expression
1 mndbn0.b 
 |-  B = ( Base ` G )
2 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
3 1 2 mndidcl 
 |-  ( G e. Mnd -> ( 0g ` G ) e. B )
4 3 ne0d 
 |-  ( G e. Mnd -> B =/= (/) )