Metamath Proof Explorer

Theorem grpbn0

Description: The base set of a group is not empty. (Contributed by Szymon Jaroszewicz, 3-Apr-2007)

Ref Expression
Hypothesis grpbn0.b 
|- B = ( Base ` G )
Assertion grpbn0 
|- ( G e. Grp -> B =/= (/) )

Proof

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