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={\mathrm{Base}}_G$$
Assertion	grpbn0	$$⊢G\in \mathrm{Grp}\to B\ne \varnothing$$

Proof

Step	Hyp	Ref	Expression
1		grpbn0.b	$$⊢B={\mathrm{Base}}_G$$
2		eqid	$$⊢0_G=0_G$$
3	1 2	grpidcl	$$⊢G\in \mathrm{Grp}\to 0_G\in B$$
4	3	ne0d	$$⊢G\in \mathrm{Grp}\to B\ne \varnothing$$