Theorem lidl1

Description: Every ring contains a unit ideal. (Contributed by Stefan O'Rear, 3-Jan-2015) (Proof shortened by AV, 18-Apr-2025)

	Ref	Expression
Hypotheses	rnglidl0.u	|- U = ( LIdeal ` R )
	rnglidl1.b	|- B = ( Base ` R )
Assertion	lidl1	|- ( R e. Ring -> B e. U )

Proof

Step	Hyp	Ref	Expression
1		rnglidl0.u	|- U = ( LIdeal ` R )
2		rnglidl1.b	|- B = ( Base ` R )
3		ringrng	|- ( R e. Ring -> R e. Rng )
4	1 2	rnglidl1	|- ( R e. Rng -> B e. U )
5	3 4	syl	|- ( R e. Ring -> B e. U )