Theorem lidlbasel

Description: An element of an ideal is an element of the ring. (Contributed by Jeff Madsen, 19-Jun-2010) (Revised by AV, 27-Jun-2026)

	Ref	Expression
Hypotheses	lidlss.b	|- B = ( Base ` W )
	lidlss.i	|- I = ( LIdeal ` W )
Assertion	lidlbasel	|- ( ( U e. I /\ X e. U ) -> X e. B )

Proof

Step	Hyp	Ref	Expression
1		lidlss.b	|- B = ( Base ` W )
2		lidlss.i	|- I = ( LIdeal ` W )
3	1 2	lidlss	|- ( U e. I -> U C_ B )
4	3	sselda	|- ( ( U e. I /\ X e. U ) -> X e. B )