This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 \in Grp \to B \neq \emptyset$

Step	Hyp	Ref	Expression
1		grpbn0.b	$⊢ B = {Base}_{G}$
2		eqid	$⊢ 0_{G} = 0_{G}$
3	1 2	grpidcl	$⊢ G \in Grp \to 0_{G} \in B$
4	3	ne0d	$⊢ G \in Grp \to B \neq \emptyset$