Metamath Proof Explorer

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 = ( Base ` G )
Assertion ringbn0 
|- ( G e. Ring -> B =/= (/) )

Proof

Step Hyp Ref Expression
1 ringbn0.b 
 |-  B = ( Base ` G )
2 ringgrp 
 |-  ( G e. Ring -> G e. Grp )
3 1 grpbn0 
 |-  ( G e. Grp -> B =/= (/) )
4 2 3 syl 
 |-  ( G e. Ring -> B =/= (/) )