Theorem ringbn0

Description: The base set of a ring is not empty. (Contributed by FL, 24-Jan-2010) (Revised by AV, 25-Aug-2011)

	Ref	Expression
Hypothesis	ringbn0.b	$$⊢B={\mathrm{Base}}_G$$
Assertion	ringbn0	$$⊢G\in \mathrm{Ring}\to B\ne \varnothing$$

Proof

Step	Hyp	Ref	Expression
1		ringbn0.b	$$⊢B={\mathrm{Base}}_G$$
2		ringgrp	$$⊢G\in \mathrm{Ring}\to G\in \mathrm{Grp}$$
3	1	grpbn0	$$⊢G\in \mathrm{Grp}\to B\ne \varnothing$$
4	2 3	syl	$$⊢G\in \mathrm{Ring}\to B\ne \varnothing$$