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	⊢ ( 𝐺 ∈ Grp → 𝐺 ≠ ∅ )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
2	1	grpbn0	⊢ ( 𝐺 ∈ Grp → ( Base ‘ 𝐺 ) ≠ ∅ )
3		fveq2	⊢ ( 𝐺 = ∅ → ( Base ‘ 𝐺 ) = ( Base ‘ ∅ ) )
4		base0	⊢ ∅ = ( Base ‘ ∅ )
5	3 4	eqtr4di	⊢ ( 𝐺 = ∅ → ( Base ‘ 𝐺 ) = ∅ )
6	5	necon3i	⊢ ( ( Base ‘ 𝐺 ) ≠ ∅ → 𝐺 ≠ ∅ )
7	2 6	syl	⊢ ( 𝐺 ∈ Grp → 𝐺 ≠ ∅ )