Metamath Proof Explorer

Theorem rngone0

Description: The base set of a ring is not empty. (Contributed by FL, 24-Jan-2010) (New usage is discouraged.)

Ref Expression
Hypotheses rngone0.1 G = 1 st R
rngone0.2 X = ran G
Assertion rngone0 R RingOps X


Step Hyp Ref Expression
1 rngone0.1 G = 1 st R
2 rngone0.2 X = ran G
3 1 rngogrpo R RingOps G GrpOp
4 2 grpon0 G GrpOp X
5 3 4 syl R RingOps X