Theorem ring0cl

Description: The zero element of a ring belongs to its base set. (Contributed by Mario Carneiro, 12-Jan-2014)

	Ref	Expression
Hypotheses	ring0cl.b	|- B = ( Base ` R )
	ring0cl.z	|- .0. = ( 0g ` R )
Assertion	ring0cl	|- ( R e. Ring -> .0. e. B )

Proof

Step	Hyp	Ref	Expression
1		ring0cl.b	|- B = ( Base ` R )
2		ring0cl.z	|- .0. = ( 0g ` R )
3		ringgrp	|- ( R e. Ring -> R e. Grp )
4	1 2	grpidcl	|- ( R e. Grp -> .0. e. B )
5	3 4	syl	|- ( R e. Ring -> .0. e. B )