Theorem grpn0

Description: A group is not empty. (Contributed by Szymon Jaroszewicz, 3-Apr-2007) (Revised by Mario Carneiro, 2-Dec-2014)

	Ref	Expression
Assertion	grpn0	$$⊢G\in \mathrm{Grp}\to G\ne \varnothing$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢{\mathrm{Base}}_G={\mathrm{Base}}_G$$
2	1	grpbn0	$$⊢G\in \mathrm{Grp}\to {\mathrm{Base}}_G\ne \varnothing$$
3		fveq2	$$⊢G=\varnothing \to {\mathrm{Base}}_G={\mathrm{Base}}_{\varnothing }$$
4		base0	$$⊢\varnothing ={\mathrm{Base}}_{\varnothing }$$
5	3 4	eqtr4di	$$⊢G=\varnothing \to {\mathrm{Base}}_G=\varnothing$$
6	5	necon3i	$$⊢{\mathrm{Base}}_G\ne \varnothing \to G\ne \varnothing$$
7	2 6	syl	$$⊢G\in \mathrm{Grp}\to G\ne \varnothing$$