Theorem rng0cl

Description: The zero element of a non-unital ring belongs to its base set. (Contributed by AV, 16-Feb-2025)

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

Proof

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